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

Theorem tfr1onlembxssdm 6194
 Description: Lemma for tfr1on 6201. 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 964 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝜑)
3 simp2 965 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝐷)
4 tfr1onlembacc.4 . . . . . . . . . 10 (𝜑𝐷𝑋)
52, 4syl 14 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝐷𝑋)
6 tfr1on.x . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
7 ordtr1 4270 . . . . . . . . . . 11 (Ord 𝑋 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
86, 7syl 14 . . . . . . . . . 10 (𝜑 → ((𝑧𝐷𝐷𝑋) → 𝑧𝑋))
98imp 123 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝐷𝑋)) → 𝑧𝑋)
102, 3, 5, 9syl12anc 1197 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧𝑋)
11 simp3l 992 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔 Fn 𝑧)
12 fneq2 5170 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓 Fn 𝑥𝑓 Fn 𝑧))
1312imbi1d 230 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
1413albidv 1778 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
15 tfr1on.ex . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
16153expia 1166 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1716alrimiv 1828 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1817ralrimiva 2479 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
1918adantr 272 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
20 simpr 109 . . . . . . . . . . 11 ((𝜑𝑧𝑋) → 𝑧𝑋)
2114, 19, 20rspcdva 2765 . . . . . . . . . 10 ((𝜑𝑧𝑋) → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
22 fneq1 5169 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
23 fveq2 5375 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
2423eleq1d 2183 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ V ↔ (𝐺𝑔) ∈ V))
2522, 24imbi12d 233 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V)))
2625spv 1814 . . . . . . . . . 10 (∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2721, 26syl 14 . . . . . . . . 9 ((𝜑𝑧𝑋) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
2827imp 123 . . . . . . . 8 (((𝜑𝑧𝑋) ∧ 𝑔 Fn 𝑧) → (𝐺𝑔) ∈ V)
292, 10, 11, 28syl21anc 1198 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝐺𝑔) ∈ V)
30 vex 2660 . . . . . . . . . 10 𝑧 ∈ V
31 opexg 4110 . . . . . . . . . 10 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
3230, 29, 31sylancr 408 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
33 snidg 3520 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → ⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩})
34 elun2 3210 . . . . . . . . 9 (⟨𝑧, (𝐺𝑔)⟩ ∈ {⟨𝑧, (𝐺𝑔)⟩} → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
3532, 33, 343syl 17 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
36 simp3r 993 . . . . . . . . . . . 12 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))
37 rspe 2455 . . . . . . . . . . . 12 ((𝑧𝑋 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
3810, 11, 36, 37syl12anc 1197 . . . . . . . . . . 11 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
39 vex 2660 . . . . . . . . . . . 12 𝑔 ∈ V
40 tfr1onlemsucfn.1 . . . . . . . . . . . . 13 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
4140tfr1onlem3ag 6188 . . . . . . . . . . . 12 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))))
4239, 41ax-mp 7 . . . . . . . . . . 11 (𝑔𝐴 ↔ ∃𝑧𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))))
4338, 42sylibr 133 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑔𝐴)
443, 11, 433jca 1144 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑧𝐷𝑔 Fn 𝑧𝑔𝐴))
45 snexg 4068 . . . . . . . . . . 11 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
46 unexg 4324 . . . . . . . . . . . 12 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4739, 46mpan 418 . . . . . . . . . . 11 ({⟨𝑧, (𝐺𝑔)⟩} ∈ V → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
4832, 45, 473syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
49 isset 2663 . . . . . . . . . 10 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V ↔ ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
5048, 49sylib 121 . . . . . . . . 9 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
51 simpr3 972 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))
52 19.8a 1552 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})) → ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
53 rspe 2455 . . . . . . . . . . . . . . 15 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
54 tfr1onlembacc.3 . . . . . . . . . . . . . . . 16 𝐵 = { ∣ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))}
5554abeq2i 2225 . . . . . . . . . . . . . . 15 (𝐵 ↔ ∃𝑧𝐷𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})))
5653, 55sylibr 133 . . . . . . . . . . . . . 14 ((𝑧𝐷 ∧ ∃𝑔(𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5752, 56sylan2 282 . . . . . . . . . . . . 13 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → 𝐵)
5851, 57eqeltrrd 2192 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ (𝑔 Fn 𝑧𝑔𝐴 = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
59583exp2 1186 . . . . . . . . . . 11 (𝑧𝐷 → (𝑔 Fn 𝑧 → (𝑔𝐴 → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))))
60593imp 1158 . . . . . . . . . 10 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → ( = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6160exlimdv 1773 . . . . . . . . 9 ((𝑧𝐷𝑔 Fn 𝑧𝑔𝐴) → (∃ = (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵))
6244, 50, 61sylc 62 . . . . . . . 8 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵)
63 elunii 3707 . . . . . . . 8 ((⟨𝑧, (𝐺𝑔)⟩ ∈ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∧ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐵) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
6435, 62, 63syl2anc 406 . . . . . . 7 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵)
65 opeq2 3672 . . . . . . . . . 10 (𝑤 = (𝐺𝑔) → ⟨𝑧, 𝑤⟩ = ⟨𝑧, (𝐺𝑔)⟩)
6665eleq1d 2183 . . . . . . . . 9 (𝑤 = (𝐺𝑔) → (⟨𝑧, 𝑤⟩ ∈ 𝐵 ↔ ⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵))
6766spcegv 2745 . . . . . . . 8 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵 → ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵))
6830eldm2 4697 . . . . . . . 8 (𝑧 ∈ dom 𝐵 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐵)
6967, 68syl6ibr 161 . . . . . . 7 ((𝐺𝑔) ∈ V → (⟨𝑧, (𝐺𝑔)⟩ ∈ 𝐵𝑧 ∈ dom 𝐵))
7029, 64, 69sylc 62 . . . . . 6 ((𝜑𝑧𝐷 ∧ (𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤)))) → 𝑧 ∈ dom 𝐵)
71703expia 1166 . . . . 5 ((𝜑𝑧𝐷) → ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7271exlimdv 1773 . . . 4 ((𝜑𝑧𝐷) → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → 𝑧 ∈ dom 𝐵))
7372ralimdva 2473 . . 3 (𝜑 → (∀𝑧𝐷𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔𝑤))) → ∀𝑧𝐷 𝑧 ∈ dom 𝐵))
741, 73mpd 13 . 2 (𝜑 → ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
75 dfss3 3053 . 2 (𝐷 ⊆ dom 𝐵 ↔ ∀𝑧𝐷 𝑧 ∈ dom 𝐵)
7674, 75sylibr 133 1 (𝜑𝐷 ⊆ dom 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 945  ∀wal 1312   = wceq 1314  ∃wex 1451   ∈ wcel 1463  {cab 2101  ∀wral 2390  ∃wrex 2391  Vcvv 2657   ∪ cun 3035   ⊆ wss 3037  {csn 3493  ⟨cop 3496  ∪ cuni 3702  Ord word 4244  suc csuc 4247  dom cdm 4499   ↾ cres 4501  Fun wfun 5075   Fn wfn 5076  ‘cfv 5081  recscrecs 6155 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-pow 4058  ax-pr 4091  ax-un 4315 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-rex 2396  df-v 2659  df-un 3041  df-in 3043  df-ss 3050  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-opab 3950  df-tr 3987  df-iord 4248  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-res 4511  df-iota 5046  df-fun 5083  df-fn 5084  df-fv 5089 This theorem is referenced by:  tfr1onlembfn  6195
 Copyright terms: Public domain W3C validator