Step | Hyp | Ref
| Expression |
1 | | bnj1463.18 |
. . . . . . 7
⊢ (𝜒 → 𝐸 ∈ 𝐵) |
2 | | elex 3185 |
. . . . . . 7
⊢ (𝐸 ∈ 𝐵 → 𝐸 ∈ V) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜒 → 𝐸 ∈ V) |
4 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑑 = 𝐸 → (𝑑 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵)) |
5 | | fneq2 5894 |
. . . . . . . . 9
⊢ (𝑑 = 𝐸 → (𝑄 Fn 𝑑 ↔ 𝑄 Fn 𝐸)) |
6 | | raleq 3115 |
. . . . . . . . 9
⊢ (𝑑 = 𝐸 → (∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊) ↔ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))) |
7 | 5, 6 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑑 = 𝐸 → ((𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)) ↔ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
8 | 4, 7 | anbi12d 743 |
. . . . . . 7
⊢ (𝑑 = 𝐸 → ((𝑑 ∈ 𝐵 ∧ (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊))) ↔ (𝐸 ∈ 𝐵 ∧ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))))) |
9 | | bnj1463.1 |
. . . . . . . . . . . 12
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
10 | 9 | bnj1317 30146 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 → ∀𝑑 𝑤 ∈ 𝐵) |
11 | 10 | nfcii 2742 |
. . . . . . . . . 10
⊢
Ⅎ𝑑𝐵 |
12 | 11 | nfel2 2767 |
. . . . . . . . 9
⊢
Ⅎ𝑑 𝐸 ∈ 𝐵 |
13 | | bnj1463.2 |
. . . . . . . . . . . . 13
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
14 | | bnj1463.3 |
. . . . . . . . . . . . 13
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
15 | | bnj1463.4 |
. . . . . . . . . . . . 13
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
16 | | bnj1463.5 |
. . . . . . . . . . . . 13
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} |
17 | | bnj1463.6 |
. . . . . . . . . . . . 13
⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) |
18 | | bnj1463.7 |
. . . . . . . . . . . . 13
⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) |
19 | | bnj1463.8 |
. . . . . . . . . . . . 13
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
20 | | bnj1463.9 |
. . . . . . . . . . . . 13
⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
21 | | bnj1463.10 |
. . . . . . . . . . . . 13
⊢ 𝑃 = ∪
𝐻 |
22 | | bnj1463.11 |
. . . . . . . . . . . . 13
⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
23 | | bnj1463.12 |
. . . . . . . . . . . . 13
⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
24 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | bnj1467 30376 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑄 → ∀𝑑 𝑤 ∈ 𝑄) |
25 | 24 | nfcii 2742 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝑄 |
26 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝐸 |
27 | 25, 26 | nffn 5901 |
. . . . . . . . . 10
⊢
Ⅎ𝑑 𝑄 Fn 𝐸 |
28 | | bnj1463.13 |
. . . . . . . . . . . . 13
⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
29 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 28 | bnj1446 30367 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑑(𝑄‘𝑧) = (𝐺‘𝑊)) |
30 | 29 | nf5i 2011 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑(𝑄‘𝑧) = (𝐺‘𝑊) |
31 | 26, 30 | nfral 2929 |
. . . . . . . . . 10
⊢
Ⅎ𝑑∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊) |
32 | 27, 31 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑑(𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)) |
33 | 12, 32 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑑(𝐸 ∈ 𝐵 ∧ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))) |
34 | 33 | nf5ri 2053 |
. . . . . . 7
⊢ ((𝐸 ∈ 𝐵 ∧ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))) → ∀𝑑(𝐸 ∈ 𝐵 ∧ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
35 | | bnj1463.17 |
. . . . . . . 8
⊢ (𝜒 → 𝑄 Fn 𝐸) |
36 | | bnj1463.16 |
. . . . . . . 8
⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)) |
37 | 1, 35, 36 | jca32 556 |
. . . . . . 7
⊢ (𝜒 → (𝐸 ∈ 𝐵 ∧ (𝑄 Fn 𝐸 ∧ ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
38 | 8, 34, 37 | bnj1465 30169 |
. . . . . 6
⊢ ((𝜒 ∧ 𝐸 ∈ V) → ∃𝑑(𝑑 ∈ 𝐵 ∧ (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
39 | 3, 38 | mpdan 699 |
. . . . 5
⊢ (𝜒 → ∃𝑑(𝑑 ∈ 𝐵 ∧ (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
40 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑑 ∈
𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)) ↔ ∃𝑑(𝑑 ∈ 𝐵 ∧ (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
41 | 39, 40 | sylibr 223 |
. . . 4
⊢ (𝜒 → ∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊))) |
42 | | bnj1463.15 |
. . . . 5
⊢ (𝜒 → 𝑄 ∈ V) |
43 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑓𝐵 |
44 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | bnj1466 30375 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑄 → ∀𝑓 𝑤 ∈ 𝑄) |
45 | 44 | nfcii 2742 |
. . . . . . . . . 10
⊢
Ⅎ𝑓𝑄 |
46 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑓𝑑 |
47 | 45, 46 | nffn 5901 |
. . . . . . . . 9
⊢
Ⅎ𝑓 𝑄 Fn 𝑑 |
48 | 9, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 28 | bnj1448 30369 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑓(𝑄‘𝑧) = (𝐺‘𝑊)) |
49 | 48 | nf5i 2011 |
. . . . . . . . . 10
⊢
Ⅎ𝑓(𝑄‘𝑧) = (𝐺‘𝑊) |
50 | 46, 49 | nfral 2929 |
. . . . . . . . 9
⊢
Ⅎ𝑓∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊) |
51 | 47, 50 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑓(𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)) |
52 | 43, 51 | nfrex 2990 |
. . . . . . 7
⊢
Ⅎ𝑓∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)) |
53 | 52 | nf5ri 2053 |
. . . . . 6
⊢
(∃𝑑 ∈
𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)) → ∀𝑓∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊))) |
54 | 25 | nfeq2 2766 |
. . . . . . 7
⊢
Ⅎ𝑑 𝑓 = 𝑄 |
55 | | fneq1 5893 |
. . . . . . . 8
⊢ (𝑓 = 𝑄 → (𝑓 Fn 𝑑 ↔ 𝑄 Fn 𝑑)) |
56 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑄 → (𝑓‘𝑧) = (𝑄‘𝑧)) |
57 | | reseq1 5311 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑄 → (𝑓 ↾ pred(𝑧, 𝐴, 𝑅)) = (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))) |
58 | 57 | opeq2d 4347 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑄 → 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉) |
59 | 58, 28 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑄 → 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉 = 𝑊) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑄 → (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉) = (𝐺‘𝑊)) |
61 | 56, 60 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑓 = 𝑄 → ((𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉) ↔ (𝑄‘𝑧) = (𝐺‘𝑊))) |
62 | 61 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑓 = 𝑄 → (∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉) ↔ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊))) |
63 | 55, 62 | anbi12d 743 |
. . . . . . 7
⊢ (𝑓 = 𝑄 → ((𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) ↔ (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
64 | 54, 63 | rexbid 3033 |
. . . . . 6
⊢ (𝑓 = 𝑄 → (∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) ↔ ∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
65 | 53, 64, 44 | bnj1468 30170 |
. . . . 5
⊢ (𝑄 ∈ V → ([𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) ↔ ∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
66 | 42, 65 | syl 17 |
. . . 4
⊢ (𝜒 → ([𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) ↔ ∃𝑑 ∈ 𝐵 (𝑄 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑄‘𝑧) = (𝐺‘𝑊)))) |
67 | 41, 66 | mpbird 246 |
. . 3
⊢ (𝜒 → [𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉))) |
68 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧)) |
69 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
70 | | bnj602 30239 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → pred(𝑥, 𝐴, 𝑅) = pred(𝑧, 𝐴, 𝑅)) |
71 | 70 | reseq2d 5317 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑓 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))) |
72 | 69, 71 | opeq12d 4348 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉) |
73 | 13, 72 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 𝑌 = 〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉) |
74 | 73 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐺‘𝑌) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) |
75 | 68, 74 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥) = (𝐺‘𝑌) ↔ (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉))) |
76 | 75 | cbvralv 3147 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑑 (𝑓‘𝑥) = (𝐺‘𝑌) ↔ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉)) |
77 | 76 | anbi2i 726 |
. . . . 5
⊢ ((𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) ↔ (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉))) |
78 | 77 | rexbii 3023 |
. . . 4
⊢
(∃𝑑 ∈
𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) ↔ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉))) |
79 | 78 | sbcbii 3458 |
. . 3
⊢
([𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) ↔ [𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑧 ∈ 𝑑 (𝑓‘𝑧) = (𝐺‘〈𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))〉))) |
80 | 67, 79 | sylibr 223 |
. 2
⊢ (𝜒 → [𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
81 | 14 | bnj1454 30166 |
. . 3
⊢ (𝑄 ∈ V → (𝑄 ∈ 𝐶 ↔ [𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))) |
82 | 42, 81 | syl 17 |
. 2
⊢ (𝜒 → (𝑄 ∈ 𝐶 ↔ [𝑄 / 𝑓]∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))) |
83 | 80, 82 | mpbird 246 |
1
⊢ (𝜒 → 𝑄 ∈ 𝐶) |