ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfrcllemsucaccv GIF version

Theorem tfrcllemsucaccv 6217
Description: Lemma for tfrcl 6227. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 24-Mar-2022.)
Hypotheses
Ref Expression
tfrcl.f 𝐹 = recs(𝐺)
tfrcl.g (𝜑 → Fun 𝐺)
tfrcl.x (𝜑 → Ord 𝑋)
tfrcl.ex ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
tfrcllemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfrcllemsucaccv.yx (𝜑𝑌𝑋)
tfrcllemsucaccv.zy (𝜑𝑧𝑌)
tfrcllemsucaccv.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfrcllemsucaccv.gfn (𝜑𝑔:𝑧𝑆)
tfrcllemsucaccv.gacc (𝜑𝑔𝐴)
Assertion
Ref Expression
tfrcllemsucaccv (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
Distinct variable groups:   𝑓,𝐺,𝑥,𝑦   𝑆,𝑓,𝑥   𝑓,𝑋,𝑥   𝑓,𝑔,𝑥,𝑦   𝜑,𝑓,𝑥,𝑦   𝑧,𝑓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧,𝑔)   𝐴(𝑥,𝑦,𝑧,𝑓,𝑔)   𝑆(𝑦,𝑧,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐺(𝑧,𝑔)   𝑋(𝑦,𝑧,𝑔)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem tfrcllemsucaccv
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 suceq 4292 . . . . 5 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
21eleq1d 2184 . . . 4 (𝑥 = 𝑧 → (suc 𝑥𝑋 ↔ suc 𝑧𝑋))
3 tfrcllemsucaccv.u . . . . 5 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
43ralrimiva 2480 . . . 4 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
5 tfrcllemsucaccv.zy . . . . 5 (𝜑𝑧𝑌)
6 tfrcllemsucaccv.yx . . . . 5 (𝜑𝑌𝑋)
7 elunii 3709 . . . . 5 ((𝑧𝑌𝑌𝑋) → 𝑧 𝑋)
85, 6, 7syl2anc 406 . . . 4 (𝜑𝑧 𝑋)
92, 4, 8rspcdva 2766 . . 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 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
155, 6jca 302 . . . . 5 (𝜑 → (𝑧𝑌𝑌𝑋))
16 ordtr1 4278 . . . . 5 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
1712, 15, 16sylc 62 . . . 4 (𝜑𝑧𝑋)
18 tfrcllemsucaccv.gfn . . . 4 (𝜑𝑔:𝑧𝑆)
19 tfrcllemsucaccv.gacc . . . 4 (𝜑𝑔𝐴)
2010, 11, 12, 13, 14, 17, 18, 19tfrcllemsucfn 6216 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆)
21 vex 2661 . . . . . 6 𝑦 ∈ V
2221elsuc 4296 . . . . 5 (𝑦 ∈ suc 𝑧 ↔ (𝑦𝑧𝑦 = 𝑧))
23 vex 2661 . . . . . . . . . . 11 𝑔 ∈ V
24 feq1 5223 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
25 fveq1 5386 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
26 reseq1 4781 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
2726fveq2d 5391 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
2825, 27eqeq12d 2130 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
2928ralbidv 2412 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3024, 29anbi12d 462 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3130rexbidv 2413 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3223, 31, 14elab2 2803 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3319, 32sylib 121 . . . . . . . . 9 (𝜑 → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
34 simprrr 512 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
35 simprrl 511 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑥𝑆)
36 ffn 5240 . . . . . . . . . . . . 13 (𝑔:𝑥𝑆𝑔 Fn 𝑥)
3735, 36syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑥)
3818adantr 272 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑧𝑆)
39 ffn 5240 . . . . . . . . . . . . 13 (𝑔:𝑧𝑆𝑔 Fn 𝑧)
4038, 39syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑧)
41 fndmu 5192 . . . . . . . . . . . 12 ((𝑔 Fn 𝑥𝑔 Fn 𝑧) → 𝑥 = 𝑧)
4237, 40, 41syl2anc 406 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑥 = 𝑧)
4342raleqdv 2607 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → (∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4434, 43mpbid 146 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4533, 44rexlimddv 2529 . . . . . . . 8 (𝜑 → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4645r19.21bi 2495 . . . . . . 7 ((𝜑𝑦𝑧) → (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
47 ordelon 4273 . . . . . . . . . . . . 13 ((Ord 𝑋𝑧𝑋) → 𝑧 ∈ On)
4812, 17, 47syl2anc 406 . . . . . . . . . . . 12 (𝜑𝑧 ∈ On)
49 onelon 4274 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦 ∈ On)
5048, 49sylan 279 . . . . . . . . . . 11 ((𝜑𝑦𝑧) → 𝑦 ∈ On)
51 eloni 4265 . . . . . . . . . . 11 (𝑦 ∈ On → Ord 𝑦)
52 ordirr 4425 . . . . . . . . . . 11 (Ord 𝑦 → ¬ 𝑦𝑦)
5350, 51, 523syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑧) → ¬ 𝑦𝑦)
54 elequ2 1674 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑦𝑧𝑦𝑦))
5554biimpcd 158 . . . . . . . . . . 11 (𝑦𝑧 → (𝑧 = 𝑦𝑦𝑦))
5655adantl 273 . . . . . . . . . 10 ((𝜑𝑦𝑧) → (𝑧 = 𝑦𝑦𝑦))
5753, 56mtod 635 . . . . . . . . 9 ((𝜑𝑦𝑧) → ¬ 𝑧 = 𝑦)
5857neqned 2290 . . . . . . . 8 ((𝜑𝑦𝑧) → 𝑧𝑦)
59 fvunsng 5580 . . . . . . . 8 ((𝑦 ∈ V ∧ 𝑧𝑦) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
6021, 58, 59sylancr 408 . . . . . . 7 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
61 eloni 4265 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
6248, 61syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
63 ordelss 4269 . . . . . . . . . . 11 ((Ord 𝑧𝑦𝑧) → 𝑦𝑧)
6462, 63sylan 279 . . . . . . . . . 10 ((𝜑𝑦𝑧) → 𝑦𝑧)
65 resabs1 4816 . . . . . . . . . 10 (𝑦𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6664, 65syl 14 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6718, 39syl 14 . . . . . . . . . . . 12 (𝜑𝑔 Fn 𝑧)
68 ordirr 4425 . . . . . . . . . . . . 13 (Ord 𝑧 → ¬ 𝑧𝑧)
6962, 68syl 14 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧𝑧)
70 fsnunres 5588 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7167, 69, 70syl2anc 406 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7271reseq1d 4786 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7372adantr 272 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7466, 73eqtr3d 2150 . . . . . . . 8 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = (𝑔𝑦))
7574fveq2d 5391 . . . . . . 7 ((𝜑𝑦𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺‘(𝑔𝑦)))
7646, 60, 753eqtr4d 2158 . . . . . 6 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
77 feq2 5224 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
7877imbi1d 230 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
7978albidv 1778 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
80133expia 1166 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8180alrimiv 1828 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8281ralrimiva 2480 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8379, 82, 17rspcdva 2766 . . . . . . . . . 10 (𝜑 → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
84 feq1 5223 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
85 fveq2 5387 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
8685eleq1d 2184 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
8784, 86imbi12d 233 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
8887spv 1814 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
8983, 18, 88sylc 62 . . . . . . . . 9 (𝜑 → (𝐺𝑔) ∈ 𝑆)
90 fndm 5190 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
9167, 90syl 14 . . . . . . . . . 10 (𝜑 → dom 𝑔 = 𝑧)
9269, 91neleqtrrd 2214 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
93 fsnunfv 5587 . . . . . . . . 9 ((𝑧𝑌 ∧ (𝐺𝑔) ∈ 𝑆 ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
945, 89, 92, 93syl3anc 1199 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
9594adantr 272 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
96 simpr 109 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → 𝑦 = 𝑧)
9796fveq2d 5391 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧))
98 reseq2 4782 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧))
9998, 71sylan9eqr 2170 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = 𝑔)
10099fveq2d 5391 . . . . . . 7 ((𝜑𝑦 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺𝑔))
10195, 97, 1003eqtr4d 2158 . . . . . 6 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10276, 101jaodan 769 . . . . 5 ((𝜑 ∧ (𝑦𝑧𝑦 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10322, 102sylan2b 283 . . . 4 ((𝜑𝑦 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
104103ralrimiva 2480 . . 3 (𝜑 → ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
105 feq2 5224 . . . . . 6 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆))
106 raleq 2601 . . . . . 6 (𝑤 = suc 𝑧 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
107105, 106anbi12d 462 . . . . 5 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
108107rspcev 2761 . . . 4 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
109 feq2 5224 . . . . . 6 (𝑤 = 𝑥 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
110 raleq 2601 . . . . . 6 (𝑤 = 𝑥 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
111109, 110anbi12d 462 . . . . 5 (𝑤 = 𝑥 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
112111cbvrexv 2630 . . . 4 (∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
113108, 112sylib 121 . . 3 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
1149, 20, 104, 113syl12anc 1197 . 2 (𝜑 → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
115 vex 2661 . . . . . 6 𝑧 ∈ V
116 opexg 4118 . . . . . 6 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
117115, 89, 116sylancr 408 . . . . 5 (𝜑 → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
118 snexg 4076 . . . . 5 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
119117, 118syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
120 unexg 4332 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
12123, 119, 120sylancr 408 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
122 feq1 5223 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓:𝑥𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
123 fveq1 5386 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦))
124 reseq1 4781 . . . . . . . . 9 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
125124fveq2d 5391 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝐺‘(𝑓𝑦)) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
126123, 125eqeq12d 2130 . . . . . . 7 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
127126ralbidv 2412 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
128122, 127anbi12d 462 . . . . 5 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
129128rexbidv 2413 . . . 4 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
130129, 14elab2g 2802 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
131121, 130syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
132114, 131mpbird 166 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 680  w3a 945  wal 1312   = wceq 1314  wcel 1463  {cab 2101  wne 2283  wral 2391  wrex 2392  Vcvv 2658  cun 3037  wss 3039  {csn 3495  cop 3498   cuni 3704  Ord word 4252  Oncon0 4253  suc csuc 4255  dom cdm 4507  cres 4509  Fun wfun 5085   Fn wfn 5086  wf 5087  cfv 5091  recscrecs 6167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099
This theorem is referenced by:  tfrcllembacc  6218  tfrcllemres  6225
  Copyright terms: Public domain W3C validator