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

Theorem tfr1onlembxssdm 6346
Description: Lemma for tfr1on 6353. 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 4390 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
86, 7syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
98imp 124 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
102, 3, 5, 9syl12anc 1236 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝑋)
11 simp3l 1025 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔 Fn 𝑧)
12 fneq2 5307 . . . . . . . . . . . . 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 2848 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
22 fneq1 5306 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
23 fveq2 5517 . . . . . . . . . . . . 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 2742 . . . . . . . . . 10 𝑧 ∈ V
31 opexg 4230 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
3230, 29, 31sylancr 414 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
33 snidg 3623 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
34 elun2 3305 . . . . . . . . 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 2742 . . . . . . . . . . . 12 𝑔 ∈ V
40 tfr1onlemsucfn.1 . . . . . . . . . . . . 13 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
4140tfr1onlem3ag 6340 . . . . . . . . . . . 12 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))))
4239, 41ax-mp 5 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
4338, 42sylibr 134 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔𝐴)
443, 11, 433jca 1177 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑧𝐷𝑔 Fn 𝑧𝑔𝐴))
45 snexg 4186 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
46 unexg 4445 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4739, 46mpan 424 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4832, 45, 473syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
49 isset 2745 . . . . . . . . . 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 3816 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
6435, 62, 63syl2anc 411 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
65 opeq2 3781 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
6665eleq1d 2246 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
6766spcegv 2827 . . . . . . . 8 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
6830eldm2 4827 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
6967, 68imbitrrdi 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 3147 . 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 2739  cun 3129  wss 3131  {csn 3594  cop 3597   cuni 3811  Ord word 4364  suc csuc 4367  dom cdm 4628  cres 4630  Fun wfun 5212   Fn wfn 5213  cfv 5218  recscrecs 6307
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 4123  ax-pow 4176  ax-pr 4211  ax-un 4435
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 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-tr 4104  df-iord 4368  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226
This theorem is referenced by:  tfr1onlembfn  6347
  Copyright terms: Public domain W3C validator