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

Theorem tfrcllembxssdm 6053
Description: Lemma for tfrcl 6061. 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 5253 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
3 reseq2 4666 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
43fveq2d 5257 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐺‘(𝑔𝑤)) = (𝐺‘(𝑔𝑦)))
52, 4eqeq12d 2097 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
65cbvralv 2583 . . . . . . 7 (∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
76anbi2i 445 . . . . . 6 ((𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
87exbii 1537 . . . . 5 (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
98ralbii 2378 . . . 4 (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
101, 9sylib 120 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
11 simp1 939 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝜑)
12 simp2 940 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝐷)
13 tfrcllembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
1411, 13syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝐷𝑋)
15 tfrcl.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
16 ordtr1 4179 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1715, 16syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1817imp 122 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
1911, 12, 14, 18syl12anc 1168 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝑋)
20 simp3l 967 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔:𝑧𝑆)
21 feq2 5099 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
2221imbi1d 229 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
2322albidv 1747 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
24 tfrcl.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25243expia 1141 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2625alrimiv 1797 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2726ralrimiva 2440 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2827adantr 270 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
29 simpr 108 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
3023, 28, 29rspcdva 2717 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
31 feq1 5098 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
32 fveq2 5253 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
3332eleq1d 2151 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
3431, 33imbi12d 232 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
3534spv 1783 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3630, 35syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3736imp 122 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
3811, 19, 20, 37syl21anc 1169 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝐺𝑔) ∈ 𝑆)
39 vex 2615 . . . . . . . . . 10 𝑧 ∈ V
40 opexg 4019 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
4139, 38, 40sylancr 405 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
42 snidg 3447 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
43 elun2 3152 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
4441, 42, 433syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
45 simp3r 968 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
46 rspe 2418 . . . . . . . . . . . . 13 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4719, 20, 45, 46syl12anc 1168 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
48 feq2 5099 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔:𝑧𝑆𝑔:𝑥𝑆))
49 raleq 2555 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5048, 49anbi12d 457 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
5150cbvrexv 2584 . . . . . . . . . . . 12 (∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5247, 51sylib 120 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
53 vex 2615 . . . . . . . . . . . 12 𝑔 ∈ V
54 feq1 5098 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
55 fveq1 5252 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
56 reseq1 4665 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
5756fveq2d 5257 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
5855, 57eqeq12d 2097 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5958ralbidv 2374 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6054, 59anbi12d 457 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
6160rexbidv 2375 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
62 tfrcllemsucfn.1 . . . . . . . . . . . 12 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6353, 61, 62elab2 2751 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6452, 63sylibr 132 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔𝐴)
6512, 20, 643jca 1119 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑧𝐷𝑔:𝑧𝑆𝑔𝐴))
66 snexg 3983 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
67 unexg 4232 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6853, 67mpan 415 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6941, 66, 683syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
70 isset 2616 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7169, 70sylib 120 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
72 simpr3 947 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
73 19.8a 1523 . . . . . . . . . . . . . 14 ((𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
74 rspe 2418 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
75 tfrcllembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7675abeq2i 2193 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7774, 76sylibr 132 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7873, 77sylan2 280 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7972, 78eqeltrrd 2160 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
80793exp2 1157 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔:𝑧𝑆 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
81803imp 1133 . . . . . . . . . 10 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8281exlimdv 1742 . . . . . . . . 9 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8365, 71, 82sylc 61 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
84 elunii 3632 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
8544, 83, 84syl2anc 403 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
86 opeq2 3597 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
8786eleq1d 2151 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
8887spcegv 2697 . . . . . . . 8 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
8939eldm2 4592 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
9088, 89syl6ibr 160 . . . . . . 7 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
9138, 85, 90sylc 61 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧 ∈ dom 𝐵)
92913expia 1141 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9392exlimdv 1742 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9493ralimdva 2435 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
9510, 94mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
96 dfss3 3000 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
9795, 96sylibr 132 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920  wal 1283   = wceq 1285  wex 1422  wcel 1434  {cab 2069  wral 2353  wrex 2354  Vcvv 2612  cun 2982  wss 2984  {csn 3422  cop 3425   cuni 3627  Ord word 4153  suc csuc 4156  dom cdm 4401  cres 4403  Fun wfun 4963  wf 4965  cfv 4969  recscrecs 6001
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 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 3922  ax-pow 3974  ax-pr 4000  ax-un 4224
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-tr 3902  df-iord 4157  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-fv 4977
This theorem is referenced by:  tfrcllembfn  6054
  Copyright terms: Public domain W3C validator