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

Theorem tfr1onlembxssdm 6322
Description: Lemma for tfr1on 6329. 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 992 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝜑)
3 simp2 993 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝐷)
4 tfr1onlembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
52, 4syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝐷𝑋)
6 tfr1on.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
7 ordtr1 4373 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
86, 7syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
98imp 123 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
102, 3, 5, 9syl12anc 1231 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝑋)
11 simp3l 1020 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔 Fn 𝑧)
12 fneq2 5287 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓 Fn 𝑥𝑓 Fn 𝑧))
1312imbi1d 230 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
1413albidv 1817 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
15 tfr1on.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
16153expia 1200 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1716alrimiv 1867 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1817ralrimiva 2543 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1918adantr 274 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
20 simpr 109 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
2114, 19, 20rspcdva 2839 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
22 fneq1 5286 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
23 fveq2 5496 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
2423eleq1d 2239 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ V ↔ (𝐺𝑔) ∈ V))
2522, 24imbi12d 233 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V)))
2625spv 1853 . . . . . . . . . 10 (∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2721, 26syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2827imp 123 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔 Fn 𝑧) → (𝐺𝑔) ∈ V)
292, 10, 11, 28syl21anc 1232 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝐺𝑔) ∈ V)
30 vex 2733 . . . . . . . . . 10 𝑧 ∈ V
31 opexg 4213 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
3230, 29, 31sylancr 412 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
33 snidg 3612 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
34 elun2 3295 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
3532, 33, 343syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
36 simp3r 1021 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))
37 rspe 2519 . . . . . . . . . . . 12 ((𝑧𝑋 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
3810, 11, 36, 37syl12anc 1231 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
39 vex 2733 . . . . . . . . . . . 12 𝑔 ∈ V
40 tfr1onlemsucfn.1 . . . . . . . . . . . . 13 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
4140tfr1onlem3ag 6316 . . . . . . . . . . . 12 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))))
4239, 41ax-mp 5 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
4338, 42sylibr 133 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔𝐴)
443, 11, 433jca 1172 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑧𝐷𝑔 Fn 𝑧𝑔𝐴))
45 snexg 4170 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
46 unexg 4428 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4739, 46mpan 422 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4832, 45, 473syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
49 isset 2736 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
5048, 49sylib 121 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
51 simpr3 1000 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
52 19.8a 1583 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
53 rspe 2519 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
54 tfr1onlembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
5554abeq2i 2281 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
5653, 55sylibr 133 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5752, 56sylan2 284 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5851, 57eqeltrrd 2248 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
59583exp2 1220 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔 Fn 𝑧 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
60593imp 1188 . . . . . . . . . 10 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6160exlimdv 1812 . . . . . . . . 9 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6244, 50, 61sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
63 elunii 3801 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
6435, 62, 63syl2anc 409 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
65 opeq2 3766 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
6665eleq1d 2239 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
6766spcegv 2818 . . . . . . . 8 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
6830eldm2 4809 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
6967, 68syl6ibr 161 . . . . . . 7 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
7029, 64, 69sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧 ∈ dom 𝐵)
71703expia 1200 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7271exlimdv 1812 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7372ralimdva 2537 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
741, 73mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
75 dfss3 3137 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
7674, 75sylibr 133 1 (𝜑𝐷 ⊆ dom 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 973  wal 1346   = wceq 1348  wex 1485  wcel 2141  {cab 2156  wral 2448  wrex 2449  Vcvv 2730  cun 3119  wss 3121  {csn 3583  cop 3586   cuni 3796  Ord word 4347  suc csuc 4350  dom cdm 4611  cres 4613  Fun wfun 5192   Fn wfn 5193  cfv 5198  recscrecs 6283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-tr 4088  df-iord 4351  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-res 4623  df-iota 5160  df-fun 5200  df-fn 5201  df-fv 5206
This theorem is referenced by:  tfr1onlembfn  6323
  Copyright terms: Public domain W3C validator