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

Theorem tfrcllembxssdm 6077
Description: Lemma for tfrcl 6085. 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 5270 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
3 reseq2 4678 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
43fveq2d 5274 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐺‘(𝑔𝑤)) = (𝐺‘(𝑔𝑦)))
52, 4eqeq12d 2099 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
65cbvralv 2586 . . . . . . 7 (∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
76anbi2i 445 . . . . . 6 ((𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
87exbii 1539 . . . . 5 (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
98ralbii 2380 . . . 4 (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
101, 9sylib 120 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
11 simp1 941 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝜑)
12 simp2 942 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝐷)
13 tfrcllembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
1411, 13syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝐷𝑋)
15 tfrcl.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
16 ordtr1 4191 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1715, 16syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1817imp 122 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
1911, 12, 14, 18syl12anc 1170 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝑋)
20 simp3l 969 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔:𝑧𝑆)
21 feq2 5113 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
2221imbi1d 229 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
2322albidv 1749 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
24 tfrcl.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25243expia 1143 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2625alrimiv 1799 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2726ralrimiva 2442 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2827adantr 270 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
29 simpr 108 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
3023, 28, 29rspcdva 2720 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
31 feq1 5112 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
32 fveq2 5270 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
3332eleq1d 2153 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
3431, 33imbi12d 232 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
3534spv 1785 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3630, 35syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3736imp 122 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
3811, 19, 20, 37syl21anc 1171 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝐺𝑔) ∈ 𝑆)
39 vex 2618 . . . . . . . . . 10 𝑧 ∈ V
40 opexg 4031 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
4139, 38, 40sylancr 405 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
42 snidg 3458 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
43 elun2 3157 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
4441, 42, 433syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
45 simp3r 970 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
46 rspe 2420 . . . . . . . . . . . . 13 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4719, 20, 45, 46syl12anc 1170 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
48 feq2 5113 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔:𝑧𝑆𝑔:𝑥𝑆))
49 raleq 2558 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5048, 49anbi12d 457 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
5150cbvrexv 2587 . . . . . . . . . . . 12 (∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5247, 51sylib 120 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
53 vex 2618 . . . . . . . . . . . 12 𝑔 ∈ V
54 feq1 5112 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
55 fveq1 5269 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
56 reseq1 4677 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
5756fveq2d 5274 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
5855, 57eqeq12d 2099 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5958ralbidv 2376 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6054, 59anbi12d 457 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
6160rexbidv 2377 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
62 tfrcllemsucfn.1 . . . . . . . . . . . 12 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6353, 61, 62elab2 2754 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6452, 63sylibr 132 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔𝐴)
6512, 20, 643jca 1121 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑧𝐷𝑔:𝑧𝑆𝑔𝐴))
66 snexg 3995 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
67 unexg 4244 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6853, 67mpan 415 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6941, 66, 683syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
70 isset 2619 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7169, 70sylib 120 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
72 simpr3 949 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
73 19.8a 1525 . . . . . . . . . . . . . 14 ((𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
74 rspe 2420 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
75 tfrcllembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7675abeq2i 2195 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7774, 76sylibr 132 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7873, 77sylan2 280 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7972, 78eqeltrrd 2162 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
80793exp2 1159 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔:𝑧𝑆 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
81803imp 1135 . . . . . . . . . 10 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8281exlimdv 1744 . . . . . . . . 9 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8365, 71, 82sylc 61 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
84 elunii 3643 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
8544, 83, 84syl2anc 403 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
86 opeq2 3608 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
8786eleq1d 2153 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
8887spcegv 2700 . . . . . . . 8 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
8939eldm2 4604 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
9088, 89syl6ibr 160 . . . . . . 7 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
9138, 85, 90sylc 61 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧 ∈ dom 𝐵)
92913expia 1143 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9392exlimdv 1744 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9493ralimdva 2437 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
9510, 94mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
96 dfss3 3004 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
9795, 96sylibr 132 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922  wal 1285   = wceq 1287  wex 1424  wcel 1436  {cab 2071  wral 2355  wrex 2356  Vcvv 2615  cun 2986  wss 2988  {csn 3431  cop 3434   cuni 3638  Ord word 4165  suc csuc 4168  dom cdm 4413  cres 4415  Fun wfun 4977  wf 4979  cfv 4983  recscrecs 6025
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-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-pow 3986  ax-pr 4012  ax-un 4236
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-opab 3877  df-tr 3914  df-iord 4169  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-fv 4991
This theorem is referenced by:  tfrcllembfn  6078
  Copyright terms: Public domain W3C validator