Step | Hyp | Ref
| Expression |
1 | | suceq 4387 |
. . . . 5
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
2 | 1 | eleq1d 2239 |
. . . 4
⊢ (𝑥 = 𝑧 → (suc 𝑥 ∈ 𝑋 ↔ suc 𝑧 ∈ 𝑋)) |
3 | | tfrcllemsucaccv.u |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) |
4 | 3 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ∪ 𝑋 suc 𝑥 ∈ 𝑋) |
5 | | tfrcllemsucaccv.zy |
. . . . 5
⊢ (𝜑 → 𝑧 ∈ 𝑌) |
6 | | tfrcllemsucaccv.yx |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
7 | | elunii 3801 |
. . . . 5
⊢ ((𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋) → 𝑧 ∈ ∪ 𝑋) |
8 | 5, 6, 7 | syl2anc 409 |
. . . 4
⊢ (𝜑 → 𝑧 ∈ ∪ 𝑋) |
9 | 2, 4, 8 | rspcdva 2839 |
. . 3
⊢ (𝜑 → suc 𝑧 ∈ 𝑋) |
10 | | tfrcl.f |
. . . 4
⊢ 𝐹 = recs(𝐺) |
11 | | tfrcl.g |
. . . 4
⊢ (𝜑 → Fun 𝐺) |
12 | | tfrcl.x |
. . . 4
⊢ (𝜑 → Ord 𝑋) |
13 | | tfrcl.ex |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) |
14 | | tfrcllemsucfn.1 |
. . . 4
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} |
15 | 5, 6 | jca 304 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋)) |
16 | | ordtr1 4373 |
. . . . 5
⊢ (Ord
𝑋 → ((𝑧 ∈ 𝑌 ∧ 𝑌 ∈ 𝑋) → 𝑧 ∈ 𝑋)) |
17 | 12, 15, 16 | sylc 62 |
. . . 4
⊢ (𝜑 → 𝑧 ∈ 𝑋) |
18 | | tfrcllemsucaccv.gfn |
. . . 4
⊢ (𝜑 → 𝑔:𝑧⟶𝑆) |
19 | | tfrcllemsucaccv.gacc |
. . . 4
⊢ (𝜑 → 𝑔 ∈ 𝐴) |
20 | 10, 11, 12, 13, 14, 17, 18, 19 | tfrcllemsucfn 6332 |
. . 3
⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):suc 𝑧⟶𝑆) |
21 | | vex 2733 |
. . . . . 6
⊢ 𝑦 ∈ V |
22 | 21 | elsuc 4391 |
. . . . 5
⊢ (𝑦 ∈ suc 𝑧 ↔ (𝑦 ∈ 𝑧 ∨ 𝑦 = 𝑧)) |
23 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
24 | | feq1 5330 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (𝑓:𝑥⟶𝑆 ↔ 𝑔:𝑥⟶𝑆)) |
25 | | fveq1 5495 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦)) |
26 | | reseq1 4885 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → (𝑓 ↾ 𝑦) = (𝑔 ↾ 𝑦)) |
27 | 26 | fveq2d 5500 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘(𝑔 ↾ 𝑦))) |
28 | 25, 27 | eqeq12d 2185 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)))) |
29 | 28 | ralbidv 2470 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)))) |
30 | 24, 29 | anbi12d 470 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) |
31 | 30 | rexbidv 2471 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) |
32 | 23, 31, 14 | elab2 2878 |
. . . . . . . . . 10
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝑋 (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)))) |
33 | 19, 32 | sylib 121 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)))) |
34 | | simprrr 535 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))) |
35 | | simprrl 534 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → 𝑔:𝑥⟶𝑆) |
36 | | ffn 5347 |
. . . . . . . . . . . . 13
⊢ (𝑔:𝑥⟶𝑆 → 𝑔 Fn 𝑥) |
37 | 35, 36 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → 𝑔 Fn 𝑥) |
38 | 18 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → 𝑔:𝑧⟶𝑆) |
39 | | ffn 5347 |
. . . . . . . . . . . . 13
⊢ (𝑔:𝑧⟶𝑆 → 𝑔 Fn 𝑧) |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → 𝑔 Fn 𝑧) |
41 | | fndmu 5299 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn 𝑥 ∧ 𝑔 Fn 𝑧) → 𝑥 = 𝑧) |
42 | 37, 40, 41 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → 𝑥 = 𝑧) |
43 | 42 | raleqdv 2671 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → (∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑧 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦)))) |
44 | 34, 43 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑔:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))))) → ∀𝑦 ∈ 𝑧 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))) |
45 | 33, 44 | rexlimddv 2592 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ 𝑧 (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))) |
46 | 45 | r19.21bi 2558 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → (𝑔‘𝑦) = (𝐺‘(𝑔 ↾ 𝑦))) |
47 | | ordelon 4368 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝑋 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ On) |
48 | 12, 17, 47 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑧 ∈ On) |
49 | | onelon 4369 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
50 | 48, 49 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
51 | | eloni 4360 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → Ord 𝑦) |
52 | | ordirr 4526 |
. . . . . . . . . . 11
⊢ (Ord
𝑦 → ¬ 𝑦 ∈ 𝑦) |
53 | 50, 51, 52 | 3syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ¬ 𝑦 ∈ 𝑦) |
54 | | elequ2 2146 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑦)) |
55 | 54 | biimpcd 158 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑧 → (𝑧 = 𝑦 → 𝑦 ∈ 𝑦)) |
56 | 55 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → (𝑧 = 𝑦 → 𝑦 ∈ 𝑦)) |
57 | 53, 56 | mtod 658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ¬ 𝑧 = 𝑦) |
58 | 57 | neqned 2347 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → 𝑧 ≠ 𝑦) |
59 | | fvunsng 5690 |
. . . . . . . 8
⊢ ((𝑦 ∈ V ∧ 𝑧 ≠ 𝑦) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝑔‘𝑦)) |
60 | 21, 58, 59 | sylancr 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝑔‘𝑦)) |
61 | | eloni 4360 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ On → Ord 𝑧) |
62 | 48, 61 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → Ord 𝑧) |
63 | | ordelss 4364 |
. . . . . . . . . . 11
⊢ ((Ord
𝑧 ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
64 | 62, 63 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
65 | | resabs1 4920 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑧 → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) |
66 | 64, 65 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) |
67 | 18, 39 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑔 Fn 𝑧) |
68 | | ordirr 4526 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑧 → ¬ 𝑧 ∈ 𝑧) |
69 | 62, 68 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑧 ∈ 𝑧) |
70 | | fsnunres 5698 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn 𝑧 ∧ ¬ 𝑧 ∈ 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) = 𝑔) |
71 | 67, 69, 70 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) = 𝑔) |
72 | 71 | reseq1d 4890 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) ↾ 𝑦) = (𝑔 ↾ 𝑦)) |
73 | 72 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧) ↾ 𝑦) = (𝑔 ↾ 𝑦)) |
74 | 66, 73 | eqtr3d 2205 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦) = (𝑔 ↾ 𝑦)) |
75 | 74 | fveq2d 5500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) = (𝐺‘(𝑔 ↾ 𝑦))) |
76 | 46, 60, 75 | 3eqtr4d 2213 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
77 | | feq2 5331 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑓:𝑥⟶𝑆 ↔ 𝑓:𝑧⟶𝑆)) |
78 | 77 | imbi1d 230 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ (𝑓:𝑧⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))) |
79 | 78 | albidv 1817 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆))) |
80 | 13 | 3expia 1200 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆)) |
81 | 80 | alrimiv 1867 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆)) |
82 | 81 | ralrimiva 2543 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑓(𝑓:𝑥⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆)) |
83 | 79, 82, 17 | rspcdva 2839 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑓(𝑓:𝑧⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆)) |
84 | | feq1 5330 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓:𝑧⟶𝑆 ↔ 𝑔:𝑧⟶𝑆)) |
85 | | fveq2 5496 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (𝐺‘𝑓) = (𝐺‘𝑔)) |
86 | 85 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((𝐺‘𝑓) ∈ 𝑆 ↔ (𝐺‘𝑔) ∈ 𝑆)) |
87 | 84, 86 | imbi12d 233 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓:𝑧⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) ↔ (𝑔:𝑧⟶𝑆 → (𝐺‘𝑔) ∈ 𝑆))) |
88 | 87 | spv 1853 |
. . . . . . . . . 10
⊢
(∀𝑓(𝑓:𝑧⟶𝑆 → (𝐺‘𝑓) ∈ 𝑆) → (𝑔:𝑧⟶𝑆 → (𝐺‘𝑔) ∈ 𝑆)) |
89 | 83, 18, 88 | sylc 62 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑔) ∈ 𝑆) |
90 | | fndm 5297 |
. . . . . . . . . . 11
⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧) |
91 | 67, 90 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑔 = 𝑧) |
92 | 69, 91 | neleqtrrd 2269 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑧 ∈ dom 𝑔) |
93 | | fsnunfv 5697 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑌 ∧ (𝐺‘𝑔) ∈ 𝑆 ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑧) = (𝐺‘𝑔)) |
94 | 5, 89, 92, 93 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝜑 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑧) = (𝐺‘𝑔)) |
95 | 94 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑧) = (𝐺‘𝑔)) |
96 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧) |
97 | 96 | fveq2d 5500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑧)) |
98 | | reseq2 4886 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑧)) |
99 | 98, 71 | sylan9eqr 2225 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦) = 𝑔) |
100 | 99 | fveq2d 5500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) = (𝐺‘𝑔)) |
101 | 95, 97, 100 | 3eqtr4d 2213 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
102 | 76, 101 | jaodan 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑧 ∨ 𝑦 = 𝑧)) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
103 | 22, 102 | sylan2b 285 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ suc 𝑧) → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
104 | 103 | ralrimiva 2543 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
105 | | feq2 5331 |
. . . . . 6
⊢ (𝑤 = suc 𝑧 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ↔ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):suc 𝑧⟶𝑆)) |
106 | | raleq 2665 |
. . . . . 6
⊢ (𝑤 = suc 𝑧 → (∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) ↔ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
107 | 105, 106 | anbi12d 470 |
. . . . 5
⊢ (𝑤 = suc 𝑧 → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ∧ ∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) ↔ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):suc 𝑧⟶𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
108 | 107 | rspcev 2834 |
. . . 4
⊢ ((suc
𝑧 ∈ 𝑋 ∧ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):suc 𝑧⟶𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) → ∃𝑤 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ∧ ∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
109 | | feq2 5331 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ↔ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆)) |
110 | | raleq 2665 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
111 | 109, 110 | anbi12d 470 |
. . . . 5
⊢ (𝑤 = 𝑥 → (((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ∧ ∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) ↔ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
112 | 111 | cbvrexv 2697 |
. . . 4
⊢
(∃𝑤 ∈
𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑤⟶𝑆 ∧ ∀𝑦 ∈ 𝑤 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
113 | 108, 112 | sylib 121 |
. . 3
⊢ ((suc
𝑧 ∈ 𝑋 ∧ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):suc 𝑧⟶𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) → ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
114 | 9, 20, 104, 113 | syl12anc 1231 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
115 | | vex 2733 |
. . . . . 6
⊢ 𝑧 ∈ V |
116 | | opexg 4213 |
. . . . . 6
⊢ ((𝑧 ∈ V ∧ (𝐺‘𝑔) ∈ 𝑆) → 〈𝑧, (𝐺‘𝑔)〉 ∈ V) |
117 | 115, 89, 116 | sylancr 412 |
. . . . 5
⊢ (𝜑 → 〈𝑧, (𝐺‘𝑔)〉 ∈ V) |
118 | | snexg 4170 |
. . . . 5
⊢
(〈𝑧, (𝐺‘𝑔)〉 ∈ V → {〈𝑧, (𝐺‘𝑔)〉} ∈ V) |
119 | 117, 118 | syl 14 |
. . . 4
⊢ (𝜑 → {〈𝑧, (𝐺‘𝑔)〉} ∈ V) |
120 | | unexg 4428 |
. . . 4
⊢ ((𝑔 ∈ V ∧ {〈𝑧, (𝐺‘𝑔)〉} ∈ V) → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V) |
121 | 23, 119, 120 | sylancr 412 |
. . 3
⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V) |
122 | | feq1 5330 |
. . . . . 6
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑓:𝑥⟶𝑆 ↔ (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆)) |
123 | | fveq1 5495 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑓‘𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦)) |
124 | | reseq1 4885 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝑓 ↾ 𝑦) = ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)) |
125 | 124 | fveq2d 5500 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (𝐺‘(𝑓 ↾ 𝑦)) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))) |
126 | 123, 125 | eqeq12d 2185 |
. . . . . . 7
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → ((𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
127 | 126 | ralbidv 2470 |
. . . . . 6
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)) ↔ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦)))) |
128 | 122, 127 | anbi12d 470 |
. . . . 5
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → ((𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
129 | 128 | rexbidv 2471 |
. . . 4
⊢ (𝑓 = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) → (∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
130 | 129, 14 | elab2g 2877 |
. . 3
⊢ ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ V → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴 ↔ ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
131 | 121, 130 | syl 14 |
. 2
⊢ (𝜑 → ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴 ↔ ∃𝑥 ∈ 𝑋 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}):𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 ((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉})‘𝑦) = (𝐺‘((𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ↾ 𝑦))))) |
132 | 114, 131 | mpbird 166 |
1
⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴) |