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

Theorem tfr1onlembxssdm 6338
Description: Lemma for tfr1on 6345. 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 4385 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
86, 7syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
98imp 124 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
102, 3, 5, 9syl12anc 1236 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝑋)
11 simp3l 1025 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔 Fn 𝑧)
12 fneq2 5301 . . . . . . . . . . . . 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 5300 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
23 fveq2 5511 . . . . . . . . . . . . 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 4225 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
3230, 29, 31sylancr 414 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
33 snidg 3620 . . . . . . . . 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 6332 . . . . . . . . . . . 12 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))))
4239, 41ax-mp 5 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
4338, 42sylibr 134 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔𝐴)
443, 11, 433jca 1177 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑧𝐷𝑔 Fn 𝑧𝑔𝐴))
45 snexg 4181 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
46 unexg 4440 . . . . . . . . . . . 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 3812 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
6435, 62, 63syl2anc 411 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
65 opeq2 3777 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
6665eleq1d 2246 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
6766spcegv 2825 . . . . . . . 8 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
6830eldm2 4821 . . . . . . . 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 3591  cop 3594   cuni 3807  Ord word 4359  suc csuc 4362  dom cdm 4623  cres 4625  Fun wfun 5206   Fn wfn 5207  cfv 5212  recscrecs 6299
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 4118  ax-pow 4171  ax-pr 4206  ax-un 4430
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 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-tr 4099  df-iord 4363  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-res 4635  df-iota 5174  df-fun 5214  df-fn 5215  df-fv 5220
This theorem is referenced by:  tfr1onlembfn  6339
  Copyright terms: Public domain W3C validator