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

Theorem tfrcllemsucaccv 6349
Description: Lemma for tfrcl 6359. 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 4399 . . . . 5 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
21eleq1d 2246 . . . 4 (𝑥 = 𝑧 → (suc 𝑥𝑋 ↔ suc 𝑧𝑋))
3 tfrcllemsucaccv.u . . . . 5 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
43ralrimiva 2550 . . . 4 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
5 tfrcllemsucaccv.zy . . . . 5 (𝜑𝑧𝑌)
6 tfrcllemsucaccv.yx . . . . 5 (𝜑𝑌𝑋)
7 elunii 3812 . . . . 5 ((𝑧𝑌𝑌𝑋) → 𝑧 𝑋)
85, 6, 7syl2anc 411 . . . 4 (𝜑𝑧 𝑋)
92, 4, 8rspcdva 2846 . . 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 306 . . . . 5 (𝜑 → (𝑧𝑌𝑌𝑋))
16 ordtr1 4385 . . . . 5 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
1712, 15, 16sylc 62 . . . 4 (𝜑𝑧𝑋)
18 tfrcllemsucaccv.gfn . . . 4 (𝜑𝑔:𝑧𝑆)
19 tfrcllemsucaccv.gacc . . . 4 (𝜑𝑔𝐴)
2010, 11, 12, 13, 14, 17, 18, 19tfrcllemsucfn 6348 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆)
21 vex 2740 . . . . . 6 𝑦 ∈ V
2221elsuc 4403 . . . . 5 (𝑦 ∈ suc 𝑧 ↔ (𝑦𝑧𝑦 = 𝑧))
23 vex 2740 . . . . . . . . . . 11 𝑔 ∈ V
24 feq1 5344 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
25 fveq1 5510 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
26 reseq1 4897 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
2726fveq2d 5515 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
2825, 27eqeq12d 2192 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
2928ralbidv 2477 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3024, 29anbi12d 473 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3130rexbidv 2478 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
3223, 31, 14elab2 2885 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
3319, 32sylib 122 . . . . . . . . 9 (𝜑 → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
34 simprrr 540 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
35 simprrl 539 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑥𝑆)
36 ffn 5361 . . . . . . . . . . . . 13 (𝑔:𝑥𝑆𝑔 Fn 𝑥)
3735, 36syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑥)
3818adantr 276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔:𝑧𝑆)
39 ffn 5361 . . . . . . . . . . . . 13 (𝑔:𝑧𝑆𝑔 Fn 𝑧)
4038, 39syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑔 Fn 𝑧)
41 fndmu 5313 . . . . . . . . . . . 12 ((𝑔 Fn 𝑥𝑔 Fn 𝑧) → 𝑥 = 𝑧)
4237, 40, 41syl2anc 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → 𝑥 = 𝑧)
4342raleqdv 2678 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → (∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4434, 43mpbid 147 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4533, 44rexlimddv 2599 . . . . . . . 8 (𝜑 → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
4645r19.21bi 2565 . . . . . . 7 ((𝜑𝑦𝑧) → (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
47 ordelon 4380 . . . . . . . . . . . . 13 ((Ord 𝑋𝑧𝑋) → 𝑧 ∈ On)
4812, 17, 47syl2anc 411 . . . . . . . . . . . 12 (𝜑𝑧 ∈ On)
49 onelon 4381 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦 ∈ On)
5048, 49sylan 283 . . . . . . . . . . 11 ((𝜑𝑦𝑧) → 𝑦 ∈ On)
51 eloni 4372 . . . . . . . . . . 11 (𝑦 ∈ On → Ord 𝑦)
52 ordirr 4538 . . . . . . . . . . 11 (Ord 𝑦 → ¬ 𝑦𝑦)
5350, 51, 523syl 17 . . . . . . . . . 10 ((𝜑𝑦𝑧) → ¬ 𝑦𝑦)
54 elequ2 2153 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑦𝑧𝑦𝑦))
5554biimpcd 159 . . . . . . . . . . 11 (𝑦𝑧 → (𝑧 = 𝑦𝑦𝑦))
5655adantl 277 . . . . . . . . . 10 ((𝜑𝑦𝑧) → (𝑧 = 𝑦𝑦𝑦))
5753, 56mtod 663 . . . . . . . . 9 ((𝜑𝑦𝑧) → ¬ 𝑧 = 𝑦)
5857neqned 2354 . . . . . . . 8 ((𝜑𝑦𝑧) → 𝑧𝑦)
59 fvunsng 5706 . . . . . . . 8 ((𝑦 ∈ V ∧ 𝑧𝑦) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
6021, 58, 59sylancr 414 . . . . . . 7 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝑔𝑦))
61 eloni 4372 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
6248, 61syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
63 ordelss 4376 . . . . . . . . . . 11 ((Ord 𝑧𝑦𝑧) → 𝑦𝑧)
6462, 63sylan 283 . . . . . . . . . 10 ((𝜑𝑦𝑧) → 𝑦𝑧)
65 resabs1 4932 . . . . . . . . . 10 (𝑦𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6664, 65syl 14 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
6718, 39syl 14 . . . . . . . . . . . 12 (𝜑𝑔 Fn 𝑧)
68 ordirr 4538 . . . . . . . . . . . . 13 (Ord 𝑧 → ¬ 𝑧𝑧)
6962, 68syl 14 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧𝑧)
70 fsnunres 5714 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7167, 69, 70syl2anc 411 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
7271reseq1d 4902 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7372adantr 276 . . . . . . . . 9 ((𝜑𝑦𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑦) = (𝑔𝑦))
7466, 73eqtr3d 2212 . . . . . . . 8 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = (𝑔𝑦))
7574fveq2d 5515 . . . . . . 7 ((𝜑𝑦𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺‘(𝑔𝑦)))
7646, 60, 753eqtr4d 2220 . . . . . 6 ((𝜑𝑦𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
77 feq2 5345 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
7877imbi1d 231 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
7978albidv 1824 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
80133expia 1205 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8180alrimiv 1874 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8281ralrimiva 2550 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
8379, 82, 17rspcdva 2846 . . . . . . . . . 10 (𝜑 → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
84 feq1 5344 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
85 fveq2 5511 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
8685eleq1d 2246 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
8784, 86imbi12d 234 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
8887spv 1860 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
8983, 18, 88sylc 62 . . . . . . . . 9 (𝜑 → (𝐺𝑔) ∈ 𝑆)
90 fndm 5311 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
9167, 90syl 14 . . . . . . . . . 10 (𝜑 → dom 𝑔 = 𝑧)
9269, 91neleqtrrd 2276 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
93 fsnunfv 5713 . . . . . . . . 9 ((𝑧𝑌 ∧ (𝐺𝑔) ∈ 𝑆 ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
945, 89, 92, 93syl3anc 1238 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
9594adantr 276 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
96 simpr 110 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → 𝑦 = 𝑧)
9796fveq2d 5515 . . . . . . 7 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧))
98 reseq2 4898 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧))
9998, 71sylan9eqr 2232 . . . . . . . 8 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦) = 𝑔)
10099fveq2d 5515 . . . . . . 7 ((𝜑𝑦 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) = (𝐺𝑔))
10195, 97, 1003eqtr4d 2220 . . . . . 6 ((𝜑𝑦 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10276, 101jaodan 797 . . . . 5 ((𝜑 ∧ (𝑦𝑧𝑦 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
10322, 102sylan2b 287 . . . 4 ((𝜑𝑦 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
104103ralrimiva 2550 . . 3 (𝜑 → ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
105 feq2 5345 . . . . . 6 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆))
106 raleq 2672 . . . . . 6 (𝑤 = suc 𝑧 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
107105, 106anbi12d 473 . . . . 5 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
108107rspcev 2841 . . . 4 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
109 feq2 5345 . . . . . 6 (𝑤 = 𝑥 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
110 raleq 2672 . . . . . 6 (𝑤 = 𝑥 → (∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
111109, 110anbi12d 473 . . . . 5 (𝑤 = 𝑥 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
112111cbvrexv 2704 . . . 4 (∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑤𝑆 ∧ ∀𝑦𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
113108, 112sylib 122 . . 3 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):suc 𝑧𝑆 ∧ ∀𝑦 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))) → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
1149, 20, 104, 113syl12anc 1236 . 2 (𝜑 → ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
115 vex 2740 . . . . . 6 𝑧 ∈ V
116 opexg 4225 . . . . . 6 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
117115, 89, 116sylancr 414 . . . . 5 (𝜑 → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
118 snexg 4181 . . . . 5 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
119117, 118syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
120 unexg 4440 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
12123, 119, 120sylancr 414 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
122 feq1 5344 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓:𝑥𝑆 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆))
123 fveq1 5510 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦))
124 reseq1 4897 . . . . . . . . 9 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑓𝑦) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))
125124fveq2d 5515 . . . . . . . 8 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝐺‘(𝑓𝑦)) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))
126123, 125eqeq12d 2192 . . . . . . 7 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
127126ralbidv 2477 . . . . . 6 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦))))
128122, 127anbi12d 473 . . . . 5 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
129128rexbidv 2478 . . . 4 (𝑓 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
130129, 14elab2g 2884 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
131121, 130syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑥𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}):𝑥𝑆 ∧ ∀𝑦𝑥 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑦) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑦)))))
132114, 131mpbird 167 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  w3a 978  wal 1351   = wceq 1353  wcel 2148  {cab 2163  wne 2347  wral 2455  wrex 2456  Vcvv 2737  cun 3127  wss 3129  {csn 3591  cop 3594   cuni 3807  Ord word 4359  Oncon0 4360  suc csuc 4362  dom cdm 4623  cres 4625  Fun wfun 5206   Fn wfn 5207  wf 5208  cfv 5212  recscrecs 6299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220
This theorem is referenced by:  tfrcllembacc  6350  tfrcllemres  6357
  Copyright terms: Public domain W3C validator