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

Theorem tfrcllembxssdm 6347
Description: Lemma for tfrcl 6355. 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 5507 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
3 reseq2 4895 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑔𝑤) = (𝑔𝑦))
43fveq2d 5511 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐺‘(𝑔𝑤)) = (𝐺‘(𝑔𝑦)))
52, 4eqeq12d 2190 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
65cbvralv 2701 . . . . . . 7 (∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
76anbi2i 457 . . . . . 6 ((𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
87exbii 1603 . . . . 5 (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
98ralbii 2481 . . . 4 (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) ↔ ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
101, 9sylib 122 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
11 simp1 997 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝜑)
12 simp2 998 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝐷)
13 tfrcllembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
1411, 13syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝐷𝑋)
15 tfrcl.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
16 ordtr1 4382 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1715, 16syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
1817imp 124 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
1911, 12, 14, 18syl12anc 1236 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧𝑋)
20 simp3l 1025 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔:𝑧𝑆)
21 feq2 5341 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓:𝑥𝑆𝑓:𝑧𝑆))
2221imbi1d 231 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
2322albidv 1822 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆)))
24 tfrcl.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25243expia 1205 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2625alrimiv 1872 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2726ralrimiva 2548 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
2827adantr 276 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
29 simpr 110 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
3023, 28, 29rspcdva 2844 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆))
31 feq1 5340 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓:𝑧𝑆𝑔:𝑧𝑆))
32 fveq2 5507 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
3332eleq1d 2244 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺𝑔) ∈ 𝑆))
3431, 33imbi12d 234 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆)))
3534spv 1858 . . . . . . . . . 10 (∀𝑓(𝑓:𝑧𝑆 → (𝐺𝑓) ∈ 𝑆) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3630, 35syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔:𝑧𝑆 → (𝐺𝑔) ∈ 𝑆))
3736imp 124 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔:𝑧𝑆) → (𝐺𝑔) ∈ 𝑆)
3811, 19, 20, 37syl21anc 1237 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝐺𝑔) ∈ 𝑆)
39 vex 2738 . . . . . . . . . 10 𝑧 ∈ V
40 opexg 4222 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ 𝑆) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
4139, 38, 40sylancr 414 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
42 snidg 3618 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
43 elun2 3301 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
4441, 42, 433syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
45 simp3r 1026 . . . . . . . . . . . . 13 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))
46 rspe 2524 . . . . . . . . . . . . 13 ((𝑧𝑋 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
4719, 20, 45, 46syl12anc 1236 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
48 feq2 5341 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑔:𝑧𝑆𝑔:𝑥𝑆))
49 raleq 2670 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5048, 49anbi12d 473 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
5150cbvrexv 2702 . . . . . . . . . . . 12 (∃𝑧𝑋 (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5247, 51sylib 122 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
53 vex 2738 . . . . . . . . . . . 12 𝑔 ∈ V
54 feq1 5340 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (𝑓:𝑥𝑆𝑔:𝑥𝑆))
55 fveq1 5506 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
56 reseq1 4894 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
5756fveq2d 5511 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑔𝑦)))
5855, 57eqeq12d 2190 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
5958ralbidv 2475 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6054, 59anbi12d 473 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → ((𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
6160rexbidv 2476 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))))
62 tfrcllemsucfn.1 . . . . . . . . . . . 12 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
6353, 61, 62elab2 2883 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑥𝑋 (𝑔:𝑥𝑆 ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝐺‘(𝑔𝑦))))
6452, 63sylibr 134 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑔𝐴)
6512, 20, 643jca 1177 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑧𝐷𝑔:𝑧𝑆𝑔𝐴))
66 snexg 4179 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
67 unexg 4437 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6853, 67mpan 424 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
6941, 66, 683syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
70 isset 2741 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
7169, 70sylib 122 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
72 simpr3 1005 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
73 19.8a 1588 . . . . . . . . . . . . . 14 ((𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
74 rspe 2524 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
75 tfrcllembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
7675abeq2i 2286 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
7774, 76sylibr 134 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7873, 77sylan2 286 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
7972, 78eqeltrrd 2253 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔:𝑧𝑆𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
80793exp2 1225 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔:𝑧𝑆 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
81803imp 1193 . . . . . . . . . 10 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8281exlimdv 1817 . . . . . . . . 9 ((𝑧𝐷𝑔:𝑧𝑆𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
8365, 71, 82sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
84 elunii 3810 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
8544, 83, 84syl2anc 411 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
86 opeq2 3775 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
8786eleq1d 2244 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
8887spcegv 2823 . . . . . . . 8 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
8939eldm2 4818 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
9088, 89syl6ibr 162 . . . . . . 7 ((𝐺𝑔) ∈ 𝑆 → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
9138, 85, 90sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦)))) → 𝑧 ∈ dom 𝐵)
92913expia 1205 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9392exlimdv 1817 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → 𝑧 ∈ dom 𝐵))
9493ralimdva 2542 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔:𝑧𝑆 ∧ ∀𝑦𝑧 (𝑔𝑦) = (𝐺‘(𝑔𝑦))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
9510, 94mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
96 dfss3 3143 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
9795, 96sylibr 134 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978  wal 1351   = wceq 1353  wex 1490  wcel 2146  {cab 2161  wral 2453  wrex 2454  Vcvv 2735  cun 3125  wss 3127  {csn 3589  cop 3592   cuni 3805  Ord word 4356  suc csuc 4359  dom cdm 4620  cres 4622  Fun wfun 5202  wf 5204  cfv 5208  recscrecs 6295
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-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-opab 4060  df-tr 4097  df-iord 4360  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-fv 5216
This theorem is referenced by:  tfrcllembfn  6348
  Copyright terms: Public domain W3C validator