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

Theorem tfrcllembxssdm 6300
 Description: Lemma for tfrcl 6308. 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 5467 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
3 reseq2 4860 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
43fveq2d 5471 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐺‘(𝑔𝑤)) = (𝐺‘(𝑔𝑦)))
52, 4eqeq12d 2172 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
65cbvralv 2680 . . . . . . 7 (∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
76anbi2i 453 . . . . . 6 ((𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
87exbii 1585 . . . . 5 (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
98ralbii 2463 . . . 4 (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
101, 9sylib 121 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
11 simp1 982 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝜑)
12 simp2 983 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝐷)
13 tfrcllembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
1411, 13syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝐷𝑋)
15 tfrcl.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
16 ordtr1 4348 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1715, 16syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1817imp 123 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
1911, 12, 14, 18syl12anc 1218 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝑋)
20 simp3l 1010 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔:𝑧𝑆)
21 feq2 5302 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
2221imbi1d 230 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
2322albidv 1804 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
24 tfrcl.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25243expia 1187 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2625alrimiv 1854 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2726ralrimiva 2530 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2827adantr 274 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
29 simpr 109 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
3023, 28, 29rspcdva 2821 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
31 feq1 5301 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
32 fveq2 5467 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
3332eleq1d 2226 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
3431, 33imbi12d 233 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
3534spv 1840 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3630, 35syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3736imp 123 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
3811, 19, 20, 37syl21anc 1219 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝐺𝑔) ∈ 𝑆)
39 vex 2715 . . . . . . . . . 10 𝑧 ∈ V
40 opexg 4188 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
4139, 38, 40sylancr 411 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
42 snidg 3589 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
43 elun2 3275 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
4441, 42, 433syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
45 simp3r 1011 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
46 rspe 2506 . . . . . . . . . . . . 13 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4719, 20, 45, 46syl12anc 1218 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
48 feq2 5302 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔:𝑧𝑆𝑔:𝑥𝑆))
49 raleq 2652 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5048, 49anbi12d 465 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
5150cbvrexv 2681 . . . . . . . . . . . 12 (∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5247, 51sylib 121 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
53 vex 2715 . . . . . . . . . . . 12 𝑔 ∈ V
54 feq1 5301 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
55 fveq1 5466 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
56 reseq1 4859 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
5756fveq2d 5471 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
5855, 57eqeq12d 2172 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5958ralbidv 2457 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6054, 59anbi12d 465 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
6160rexbidv 2458 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
62 tfrcllemsucfn.1 . . . . . . . . . . . 12 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6353, 61, 62elab2 2860 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6452, 63sylibr 133 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔𝐴)
6512, 20, 643jca 1162 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑧𝐷𝑔:𝑧𝑆𝑔𝐴))
66 snexg 4145 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
67 unexg 4402 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6853, 67mpan 421 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6941, 66, 683syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
70 isset 2718 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7169, 70sylib 121 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
72 simpr3 990 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
73 19.8a 1570 . . . . . . . . . . . . . 14 ((𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
74 rspe 2506 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
75 tfrcllembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7675abeq2i 2268 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7774, 76sylibr 133 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7873, 77sylan2 284 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7972, 78eqeltrrd 2235 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
80793exp2 1207 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔:𝑧𝑆 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
81803imp 1176 . . . . . . . . . 10 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8281exlimdv 1799 . . . . . . . . 9 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8365, 71, 82sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
84 elunii 3777 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
8544, 83, 84syl2anc 409 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
86 opeq2 3742 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
8786eleq1d 2226 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
8887spcegv 2800 . . . . . . . 8 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
8939eldm2 4783 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
9088, 89syl6ibr 161 . . . . . . 7 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
9138, 85, 90sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧 ∈ dom 𝐵)
92913expia 1187 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9392exlimdv 1799 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9493ralimdva 2524 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
9510, 94mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
96 dfss3 3118 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
9795, 96sylibr 133 1 (𝜑𝐷 ⊆ dom 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963  ∀wal 1333   = wceq 1335  ∃wex 1472   ∈ wcel 2128  {cab 2143  ∀wral 2435  ∃wrex 2436  Vcvv 2712   ∪ cun 3100   ⊆ wss 3102  {csn 3560  ⟨cop 3563  ∪ cuni 3772  Ord word 4322  suc csuc 4325  dom cdm 4585   ↾ cres 4587  Fun wfun 5163  ⟶wf 5165  ‘cfv 5169  recscrecs 6248 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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-tr 4063  df-iord 4326  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-fv 5177 This theorem is referenced by:  tfrcllembfn  6301
 Copyright terms: Public domain W3C validator