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

Theorem tfrcllembxssdm 6219
Description: Lemma for tfrcl 6227. The union of 𝐵 is defined on all elements of 𝑋. (Contributed by Jim Kingdon, 25-Mar-2022.)
Hypotheses
Ref Expression
tfrcl.f 𝐹 = recs(𝐺)
tfrcl.g (𝜑 → Fun 𝐺)
tfrcl.x (𝜑 → Ord 𝑋)
tfrcl.ex ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
tfrcllemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfrcllembacc.3 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
tfrcllembacc.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfrcllembacc.4 (𝜑𝐷𝑋)
tfrcllembacc.5 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
Assertion
Ref Expression
tfrcllembxssdm (𝜑𝐷 ⊆ dom 𝐵)
Distinct variable groups:   𝐴,𝑓,𝑔,,𝑥,𝑦,𝑧   𝐷,𝑓,𝑔,𝑥,𝑦   𝑓,𝐺,𝑥,𝑦   𝑆,𝑓,𝑥,𝑦   𝑓,𝑋,𝑥   𝜑,𝑓,𝑔,,𝑥,𝑦,𝑧   𝐵,𝑔,,𝑧   𝑤,𝐵,𝑔,𝑧   𝐷,,𝑧   ,𝐺,𝑧   𝑤,𝐺,𝑦   𝑆,,𝑧   𝑧,𝑋
Allowed substitution hints:   𝜑(𝑤)   𝐴(𝑤)   𝐵(𝑥,𝑦,𝑓)   𝐷(𝑤)   𝑆(𝑤,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔,)   𝐺(𝑔)   𝑋(𝑦,𝑤,𝑔,)

Proof of Theorem tfrcllembxssdm
StepHypRef Expression
1 tfrcllembacc.5 . . . 4 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
2 fveq2 5387 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
3 reseq2 4782 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
43fveq2d 5391 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐺‘(𝑔𝑤)) = (𝐺‘(𝑔𝑦)))
52, 4eqeq12d 2130 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
65cbvralv 2629 . . . . . . 7 (∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
76anbi2i 450 . . . . . 6 ((𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
87exbii 1567 . . . . 5 (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
98ralbii 2416 . . . 4 (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
101, 9sylib 121 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
11 simp1 964 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝜑)
12 simp2 965 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝐷)
13 tfrcllembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
1411, 13syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝐷𝑋)
15 tfrcl.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
16 ordtr1 4278 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1715, 16syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1817imp 123 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
1911, 12, 14, 18syl12anc 1197 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝑋)
20 simp3l 992 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔:𝑧𝑆)
21 feq2 5224 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
2221imbi1d 230 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
2322albidv 1778 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
24 tfrcl.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25243expia 1166 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2625alrimiv 1828 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2726ralrimiva 2480 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2827adantr 272 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
29 simpr 109 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
3023, 28, 29rspcdva 2766 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
31 feq1 5223 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
32 fveq2 5387 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
3332eleq1d 2184 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
3431, 33imbi12d 233 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
3534spv 1814 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3630, 35syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3736imp 123 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
3811, 19, 20, 37syl21anc 1198 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝐺𝑔) ∈ 𝑆)
39 vex 2661 . . . . . . . . . 10 𝑧 ∈ V
40 opexg 4118 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
4139, 38, 40sylancr 408 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
42 snidg 3522 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
43 elun2 3212 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
4441, 42, 433syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
45 simp3r 993 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
46 rspe 2456 . . . . . . . . . . . . 13 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4719, 20, 45, 46syl12anc 1197 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
48 feq2 5224 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔:𝑧𝑆𝑔:𝑥𝑆))
49 raleq 2601 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5048, 49anbi12d 462 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
5150cbvrexv 2630 . . . . . . . . . . . 12 (∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5247, 51sylib 121 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
53 vex 2661 . . . . . . . . . . . 12 𝑔 ∈ V
54 feq1 5223 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
55 fveq1 5386 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
56 reseq1 4781 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
5756fveq2d 5391 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
5855, 57eqeq12d 2130 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5958ralbidv 2412 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6054, 59anbi12d 462 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
6160rexbidv 2413 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
62 tfrcllemsucfn.1 . . . . . . . . . . . 12 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6353, 61, 62elab2 2803 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6452, 63sylibr 133 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔𝐴)
6512, 20, 643jca 1144 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑧𝐷𝑔:𝑧𝑆𝑔𝐴))
66 snexg 4076 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
67 unexg 4332 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6853, 67mpan 418 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6941, 66, 683syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
70 isset 2664 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7169, 70sylib 121 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
72 simpr3 972 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
73 19.8a 1552 . . . . . . . . . . . . . 14 ((𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
74 rspe 2456 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
75 tfrcllembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7675abeq2i 2226 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7774, 76sylibr 133 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7873, 77sylan2 282 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7972, 78eqeltrrd 2193 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
80793exp2 1186 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔:𝑧𝑆 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
81803imp 1158 . . . . . . . . . 10 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8281exlimdv 1773 . . . . . . . . 9 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8365, 71, 82sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
84 elunii 3709 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
8544, 83, 84syl2anc 406 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
86 opeq2 3674 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
8786eleq1d 2184 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
8887spcegv 2746 . . . . . . . 8 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
8939eldm2 4705 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
9088, 89syl6ibr 161 . . . . . . 7 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
9138, 85, 90sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧 ∈ dom 𝐵)
92913expia 1166 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9392exlimdv 1773 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9493ralimdva 2474 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
9510, 94mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
96 dfss3 3055 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
9795, 96sylibr 133 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945  wal 1312   = wceq 1314  wex 1451  wcel 1463  {cab 2101  wral 2391  wrex 2392  Vcvv 2658  cun 3037  wss 3039  {csn 3495  cop 3498   cuni 3704  Ord word 4252  suc csuc 4255  dom cdm 4507  cres 4509  Fun wfun 5085  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-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
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  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-iord 4256  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-fv 5099
This theorem is referenced by:  tfrcllembfn  6220
  Copyright terms: Public domain W3C validator