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

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

Proof of Theorem tfr1onlembxssdm
StepHypRef Expression
1 tfr1onlembacc.5 . . 3 (𝜑 → ∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
2 simp1 997 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝜑)
3 simp2 998 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝐷)
4 tfr1onlembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
52, 4syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝐷𝑋)
6 tfr1on.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
7 ordtr1 4388 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
86, 7syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
98imp 124 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
102, 3, 5, 9syl12anc 1236 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝑋)
11 simp3l 1025 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔 Fn 𝑧)
12 fneq2 5305 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓 Fn 𝑥𝑓 Fn 𝑧))
1312imbi1d 231 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
1413albidv 1824 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
15 tfr1on.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
16153expia 1205 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1716alrimiv 1874 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1817ralrimiva 2550 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1918adantr 276 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
20 simpr 110 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
2114, 19, 20rspcdva 2846 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
22 fneq1 5304 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
23 fveq2 5515 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
2423eleq1d 2246 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ V ↔ (𝐺𝑔) ∈ V))
2522, 24imbi12d 234 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V)))
2625spv 1860 . . . . . . . . . 10 (∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2721, 26syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2827imp 124 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔 Fn 𝑧) → (𝐺𝑔) ∈ V)
292, 10, 11, 28syl21anc 1237 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝐺𝑔) ∈ V)
30 vex 2740 . . . . . . . . . 10 𝑧 ∈ V
31 opexg 4228 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
3230, 29, 31sylancr 414 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
33 snidg 3621 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
34 elun2 3303 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
3532, 33, 343syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
36 simp3r 1026 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))
37 rspe 2526 . . . . . . . . . . . 12 ((𝑧𝑋 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
3810, 11, 36, 37syl12anc 1236 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
39 vex 2740 . . . . . . . . . . . 12 𝑔 ∈ V
40 tfr1onlemsucfn.1 . . . . . . . . . . . . 13 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
4140tfr1onlem3ag 6337 . . . . . . . . . . . 12 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))))
4239, 41ax-mp 5 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
4338, 42sylibr 134 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔𝐴)
443, 11, 433jca 1177 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑧𝐷𝑔 Fn 𝑧𝑔𝐴))
45 snexg 4184 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
46 unexg 4443 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4739, 46mpan 424 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4832, 45, 473syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
49 isset 2743 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
5048, 49sylib 122 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
51 simpr3 1005 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
52 19.8a 1590 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
53 rspe 2526 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
54 tfr1onlembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
5554abeq2i 2288 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
5653, 55sylibr 134 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5752, 56sylan2 286 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5851, 57eqeltrrd 2255 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
59583exp2 1225 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔 Fn 𝑧 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
60593imp 1193 . . . . . . . . . 10 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6160exlimdv 1819 . . . . . . . . 9 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6244, 50, 61sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
63 elunii 3814 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
6435, 62, 63syl2anc 411 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
65 opeq2 3779 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
6665eleq1d 2246 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
6766spcegv 2825 . . . . . . . 8 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
6830eldm2 4825 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
6967, 68syl6ibr 162 . . . . . . 7 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
7029, 64, 69sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧 ∈ dom 𝐵)
71703expia 1205 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7271exlimdv 1819 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7372ralimdva 2544 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
741, 73mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
75 dfss3 3145 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
7674, 75sylibr 134 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978  wal 1351   = wceq 1353  wex 1492  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2737  cun 3127  wss 3129  {csn 3592  cop 3595   cuni 3809  Ord word 4362  suc csuc 4365  dom cdm 4626  cres 4628  Fun wfun 5210   Fn wfn 5211  cfv 5216  recscrecs 6304
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-tr 4102  df-iord 4366  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-res 4638  df-iota 5178  df-fun 5218  df-fn 5219  df-fv 5224
This theorem is referenced by:  tfr1onlembfn  6344
  Copyright terms: Public domain W3C validator