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

Theorem tfrcllemsucaccv 6023
 Description: Lemma for tfrcl 6033. 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 4185 . . . . 5 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
21eleq1d 2151 . . . 4 (𝑥 = 𝑧 → (suc 𝑥𝑋 ↔ suc 𝑧𝑋))
3 tfrcllemsucaccv.u . . . . 5 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
43ralrimiva 2439 . . . 4 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
5 tfrcllemsucaccv.zy . . . . 5 (𝜑𝑧𝑌)
6 tfrcllemsucaccv.yx . . . . 5 (𝜑𝑌𝑋)
7 elunii 3626 . . . . 5 ((𝑧𝑌𝑌𝑋) → 𝑧 𝑋)
85, 6, 7syl2anc 403 . . . 4 (𝜑𝑧 𝑋)
92, 4, 8rspcdva 2715 . . 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 300 . . . . 5 (𝜑 → (𝑧𝑌𝑌𝑋))
16 ordtr1 4171 . . . . 5 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
1712, 15, 16sylc 61 . . . 4 (𝜑𝑧𝑋)
18 tfrcllemsucaccv.gfn . . . 4 (𝜑𝑔:𝑧𝑆)
19 tfrcllemsucaccv.gacc . . . 4 (𝜑𝑔𝐴)
2010, 11, 12, 13, 14, 17, 18, 19tfrcllemsucfn 6022 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆)
21 vex 2613 . . . . . 6 𝑦 ∈ V
2221elsuc 4189 . . . . 5 (𝑦 ∈ suc 𝑧 ↔ (𝑦𝑧𝑦 = 𝑧))
23 vex 2613 . . . . . . . . . . 11 𝑔 ∈ V
24 feq1 5081 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
25 fveq1 5228 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
26 reseq1 4654 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
2726fveq2d 5233 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
2825, 27eqeq12d 2097 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
2928ralbidv 2373 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3024, 29anbi12d 457 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3130rexbidv 2374 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3223, 31, 14elab2 2749 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3319, 32sylib 120 . . . . . . . . 9 (𝜑 → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
34 simprrr 507 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
35 simprrl 506 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑥𝑆)
36 ffn 5097 . . . . . . . . . . . . 13 (𝑔:𝑥𝑆𝑔 Fn 𝑥)
3735, 36syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑥)
3818adantr 270 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑧𝑆)
39 ffn 5097 . . . . . . . . . . . . 13 (𝑔:𝑧𝑆𝑔 Fn 𝑧)
4038, 39syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑧)
41 fndmu 5051 . . . . . . . . . . . 12 ((𝑔 Fn 𝑥𝑔 Fn 𝑧) → 𝑥 = 𝑧)
4237, 40, 41syl2anc 403 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑥 = 𝑧)
4342raleqdv 2560 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → (∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4434, 43mpbid 145 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4533, 44rexlimddv 2486 . . . . . . . 8 (𝜑 → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4645r19.21bi 2454 . . . . . . 7 ((𝜑𝑦𝑧) → (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
47 ordelon 4166 . . . . . . . . . . . . 13 ((Ord 𝑋𝑧𝑋) → 𝑧 ∈ On)
4812, 17, 47syl2anc 403 . . . . . . . . . . . 12 (𝜑𝑧 ∈ On)
49 onelon 4167 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦 ∈ On)
5048, 49sylan 277 . . . . . . . . . . 11 ((𝜑𝑦𝑧) → 𝑦 ∈ On)
51 eloni 4158 . . . . . . . . . . 11 (𝑦 ∈ On → Ord 𝑦)
52 ordirr 4313 . . . . . . . . . . 11 (Ord 𝑦 → ¬ 𝑦𝑦)
5350, 51, 523syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑧) → ¬ 𝑦𝑦)
54 elequ2 1643 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑦𝑧𝑦𝑦))
5554biimpcd 157 . . . . . . . . . . 11 (𝑦𝑧 → (𝑧 = 𝑦𝑦𝑦))
5655adantl 271 . . . . . . . . . 10 ((𝜑𝑦𝑧) → (𝑧 = 𝑦𝑦𝑦))
5753, 56mtod 622 . . . . . . . . 9 ((𝜑𝑦𝑧) → ¬ 𝑧 = 𝑦)
5857neqned 2256 . . . . . . . 8 ((𝜑𝑦𝑧) → 𝑧𝑦)
59 fvunsng 5409 . . . . . . . 8 ((𝑦 ∈ V ∧ 𝑧𝑦) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
6021, 58, 59sylancr 405 . . . . . . 7 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
61 eloni 4158 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
6248, 61syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
63 ordelss 4162 . . . . . . . . . . 11 ((Ord 𝑧𝑦𝑧) → 𝑦𝑧)
6462, 63sylan 277 . . . . . . . . . 10 ((𝜑𝑦𝑧) → 𝑦𝑧)
65 resabs1 4688 . . . . . . . . . 10 (𝑦𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6664, 65syl 14 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6718, 39syl 14 . . . . . . . . . . . 12 (𝜑𝑔 Fn 𝑧)
68 ordirr 4313 . . . . . . . . . . . . 13 (Ord 𝑧 → ¬ 𝑧𝑧)
6962, 68syl 14 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧𝑧)
70 fsnunres 5416 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7167, 69, 70syl2anc 403 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7271reseq1d 4659 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7372adantr 270 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7466, 73eqtr3d 2117 . . . . . . . 8 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = (𝑔𝑦))
7574fveq2d 5233 . . . . . . 7 ((𝜑𝑦𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺‘(𝑔𝑦)))
7646, 60, 753eqtr4d 2125 . . . . . 6 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
77 feq2 5082 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
7877imbi1d 229 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
7978albidv 1747 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
80133expia 1141 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8180alrimiv 1797 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8281ralrimiva 2439 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8379, 82, 17rspcdva 2715 . . . . . . . . . 10 (𝜑 → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
84 feq1 5081 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
85 fveq2 5229 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
8685eleq1d 2151 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
8784, 86imbi12d 232 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
8887spv 1783 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
8983, 18, 88sylc 61 . . . . . . . . 9 (𝜑 → (𝐺𝑔) ∈ 𝑆)
90 fndm 5049 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
9167, 90syl 14 . . . . . . . . . 10 (𝜑 → dom 𝑔 = 𝑧)
9269, 91neleqtrrd 2181 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
93 fsnunfv 5415 . . . . . . . . 9 ((𝑧𝑌 ∧ (𝐺𝑔) ∈ 𝑆 ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
945, 89, 92, 93syl3anc 1170 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
9594adantr 270 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
96 simpr 108 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → 𝑦 = 𝑧)
9796fveq2d 5233 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧))
98 reseq2 4655 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧))
9998, 71sylan9eqr 2137 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = 𝑔)
10099fveq2d 5233 . . . . . . 7 ((𝜑𝑦 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺𝑔))
10195, 97, 1003eqtr4d 2125 . . . . . 6 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10276, 101jaodan 744 . . . . 5 ((𝜑 ∧ (𝑦𝑧𝑦 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10322, 102sylan2b 281 . . . 4 ((𝜑𝑦 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
104103ralrimiva 2439 . . 3 (𝜑 → ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
105 feq2 5082 . . . . . 6 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆))
106 raleq 2554 . . . . . 6 (𝑤 = suc 𝑧 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
107105, 106anbi12d 457 . . . . 5 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
108107rspcev 2710 . . . 4 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
109 feq2 5082 . . . . . 6 (𝑤 = 𝑥 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
110 raleq 2554 . . . . . 6 (𝑤 = 𝑥 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
111109, 110anbi12d 457 . . . . 5 (𝑤 = 𝑥 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
112111cbvrexv 2583 . . . 4 (∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
113108, 112sylib 120 . . 3 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
1149, 20, 104, 113syl12anc 1168 . 2 (𝜑 → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
115 vex 2613 . . . . . 6 𝑧 ∈ V
116 opexg 4011 . . . . . 6 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
117115, 89, 116sylancr 405 . . . . 5 (𝜑 → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
118 snexg 3976 . . . . 5 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
119117, 118syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
120 unexg 4224 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
12123, 119, 120sylancr 405 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
122 feq1 5081 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓:𝑥𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
123 fveq1 5228 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦))
124 reseq1 4654 . . . . . . . . 9 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
125124fveq2d 5233 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝐺‘(𝑓𝑦)) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
126123, 125eqeq12d 2097 . . . . . . 7 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
127126ralbidv 2373 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
128122, 127anbi12d 457 . . . . 5 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
129128rexbidv 2374 . . . 4 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
130129, 14elab2g 2748 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
131121, 130syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
132114, 131mpbird 165 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662   ∧ w3a 920  ∀wal 1283   = wceq 1285   ∈ wcel 1434  {cab 2069   ≠ wne 2249  ∀wral 2353  ∃wrex 2354  Vcvv 2610   ∪ cun 2980   ⊆ wss 2982  {csn 3416  ⟨cop 3419  ∪ cuni 3621  Ord word 4145  Oncon0 4146  suc csuc 4148  dom cdm 4391   ↾ cres 4393  Fun wfun 4946   Fn wfn 4947  ⟶wf 4948  ‘cfv 4952  recscrecs 5973 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308 This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-v 2612  df-sbc 2825  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-tr 3896  df-id 4076  df-iord 4149  df-on 4151  df-suc 4154  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-fo 4958  df-f1o 4959  df-fv 4960 This theorem is referenced by:  tfrcllembacc  6024  tfrcllemres  6031
 Copyright terms: Public domain W3C validator