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

Theorem exmidonfinlem 7186
Description: Lemma for exmidonfin 7187. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
Hypothesis
Ref Expression
exmidonfinlem.a 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
Assertion
Ref Expression
exmidonfinlem (ω = (On ∩ Fin) → DECID 𝜑)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem exmidonfinlem
Dummy variables 𝑟 𝑠 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpri 3614 . . . . . . . . . 10 (𝑟 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2 exmidonfinlem.a . . . . . . . . . 10 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
31, 2eleq2s 2272 . . . . . . . . 9 (𝑟𝐴 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
4 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
54biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
6 elrabi 2890 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {∅})
7 velsn 3608 . . . . . . . . . . . . . 14 (𝑠 ∈ {∅} ↔ 𝑠 = ∅)
86, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = ∅)
9 biidd 172 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (𝜑𝜑))
109elrab 2893 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (𝑠 ∈ {∅} ∧ 𝜑))
1110simprbi 275 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
1211notnotd 630 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ ¬ 𝜑)
13 0ex 4127 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
1413snm 3711 . . . . . . . . . . . . . . . 16 𝑤 𝑤 ∈ {∅}
15 r19.3rmv 3513 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑))
1614, 15ax-mp 5 . . . . . . . . . . . . . . 15 (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1712, 16sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
18 rabeq0 3452 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1917, 18sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → {𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅)
208, 19eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
21 p0ex 4185 . . . . . . . . . . . . . . 15 {∅} ∈ V
2221rabex 4144 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V
2322prid2 3698 . . . . . . . . . . . . 13 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
2423, 2eleqtrri 2253 . . . . . . . . . . . 12 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ 𝐴
2520, 24eqeltrdi 2268 . . . . . . . . . . 11 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴)
265, 25syl6 33 . . . . . . . . . 10 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴))
27 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2827biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
29 elrabi 2890 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {∅})
3029, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = ∅)
31 biidd 172 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (¬ 𝜑 ↔ ¬ 𝜑))
3231elrab 2893 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ↔ (𝑠 ∈ {∅} ∧ ¬ 𝜑))
3332simprbi 275 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ¬ 𝜑)
34 r19.3rmv 3513 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑))
3514, 34ax-mp 5 . . . . . . . . . . . . . . 15 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3633, 35sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∀𝑥 ∈ {∅} ¬ 𝜑)
37 rabeq0 3452 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3836, 37sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → {𝑥 ∈ {∅} ∣ 𝜑} = ∅)
3930, 38eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ 𝜑})
4021rabex 4144 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ 𝜑} ∈ V
4140prid1 3697 . . . . . . . . . . . . 13 {𝑥 ∈ {∅} ∣ 𝜑} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
4241, 2eleqtrri 2253 . . . . . . . . . . . 12 {𝑥 ∈ {∅} ∣ 𝜑} ∈ 𝐴
4339, 42eqeltrdi 2268 . . . . . . . . . . 11 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠𝐴)
4428, 43syl6 33 . . . . . . . . . 10 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠𝐴))
4526, 44jaod 717 . . . . . . . . 9 (𝑠𝑟 → ((𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → 𝑠𝐴))
463, 45mpan9 281 . . . . . . . 8 ((𝑟𝐴𝑠𝑟) → 𝑠𝐴)
4746rgen2 2563 . . . . . . 7 𝑟𝐴𝑠𝑟 𝑠𝐴
48 dftr5 4101 . . . . . . 7 (Tr 𝐴 ↔ ∀𝑟𝐴𝑠𝑟 𝑠𝐴)
4947, 48mpbir 146 . . . . . 6 Tr 𝐴
50 elpri 3614 . . . . . . . . 9 (𝑧 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5150, 2eleq2s 2272 . . . . . . . 8 (𝑧𝐴 → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
52 ordtriexmidlem 4515 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ 𝜑} ∈ On
5352ontrci 4424 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ 𝜑}
54 treq 4104 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ 𝜑}))
5553, 54mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → Tr 𝑧)
56 ordtriexmidlem 4515 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ On
5756ontrci 4424 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}
58 treq 4104 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5957, 58mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → Tr 𝑧)
6055, 59jaoi 716 . . . . . . . 8 ((𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → Tr 𝑧)
6151, 60syl 14 . . . . . . 7 (𝑧𝐴 → Tr 𝑧)
6261rgen 2530 . . . . . 6 𝑧𝐴 Tr 𝑧
63 dford3 4364 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑧𝐴 Tr 𝑧))
6449, 62, 63mpbir2an 942 . . . . 5 Ord 𝐴
65 prexg 4208 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V)
6640, 22, 65mp2an 426 . . . . . . 7 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V
672, 66eqeltri 2250 . . . . . 6 𝐴 ∈ V
6867elon 4371 . . . . 5 (𝐴 ∈ On ↔ Ord 𝐴)
6964, 68mpbir 146 . . . 4 𝐴 ∈ On
70 2onn 6516 . . . . . 6 2o ∈ ω
71 nnfi 6866 . . . . . 6 (2o ∈ ω → 2o ∈ Fin)
7270, 71ax-mp 5 . . . . 5 2o ∈ Fin
73 pm5.19 706 . . . . . . . . . 10 ¬ (𝜑 ↔ ¬ 𝜑)
7413snm 3711 . . . . . . . . . . 11 𝑦 𝑦 ∈ {∅}
75 r19.3rmv 3513 . . . . . . . . . . 11 (∃𝑦 𝑦 ∈ {∅} → ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)))
7674, 75ax-mp 5 . . . . . . . . . 10 ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑))
7773, 76mtbi 670 . . . . . . . . 9 ¬ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)
78 rabbi 2654 . . . . . . . . 9 (∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑) ↔ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
7977, 78mtbi 670 . . . . . . . 8 ¬ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}
8079neir 2350 . . . . . . 7 {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}
81 pr2ne 7185 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
8240, 22, 81mp2an 426 . . . . . . 7 ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
8380, 82mpbir 146 . . . . . 6 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o
842, 83eqbrtri 4021 . . . . 5 𝐴 ≈ 2o
85 enfii 6868 . . . . 5 ((2o ∈ Fin ∧ 𝐴 ≈ 2o) → 𝐴 ∈ Fin)
8672, 84, 85mp2an 426 . . . 4 𝐴 ∈ Fin
8769, 86elini 3319 . . 3 𝐴 ∈ (On ∩ Fin)
88 eleq2 2241 . . 3 (ω = (On ∩ Fin) → (𝐴 ∈ ω ↔ 𝐴 ∈ (On ∩ Fin)))
8987, 88mpbiri 168 . 2 (ω = (On ∩ Fin) → 𝐴 ∈ ω)
90 df1o2 6424 . . . . 5 1o = {∅}
91 1lt2o 6437 . . . . 5 1o ∈ 2o
9290, 91eqeltrri 2251 . . . 4 {∅} ∈ 2o
93 nneneq 6851 . . . . . 6 ((𝐴 ∈ ω ∧ 2o ∈ ω) → (𝐴 ≈ 2o𝐴 = 2o))
9470, 93mpan2 425 . . . . 5 (𝐴 ∈ ω → (𝐴 ≈ 2o𝐴 = 2o))
9584, 94mpbii 148 . . . 4 (𝐴 ∈ ω → 𝐴 = 2o)
9692, 95eleqtrrid 2267 . . 3 (𝐴 ∈ ω → {∅} ∈ 𝐴)
97 elpri 3614 . . . 4 ({∅} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9897, 2eleq2s 2272 . . 3 ({∅} ∈ 𝐴 → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9996, 98syl 14 . 2 (𝐴 ∈ ω → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
10013snid 3622 . . . . . . 7 ∅ ∈ {∅}
101 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
102100, 101mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑})
103 biidd 172 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜑))
104103elrab 2893 . . . . . 6 (∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (∅ ∈ {∅} ∧ 𝜑))
105102, 104sylib 122 . . . . 5 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ∧ 𝜑))
106105simprd 114 . . . 4 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
107 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
108100, 107mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
109 biidd 172 . . . . . . 7 (𝑥 = ∅ → (¬ 𝜑 ↔ ¬ 𝜑))
110109elrab 2893 . . . . . 6 (∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ↔ (∅ ∈ {∅} ∧ ¬ 𝜑))
111108, 110sylib 122 . . . . 5 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (∅ ∈ {∅} ∧ ¬ 𝜑))
112111simprd 114 . . . 4 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ¬ 𝜑)
113106, 112orim12i 759 . . 3 (({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → (𝜑 ∨ ¬ 𝜑))
114 df-dc 835 . . 3 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
115113, 114sylibr 134 . 2 (({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → DECID 𝜑)
11689, 99, 1153syl 17 1 (ω = (On ∩ Fin) → DECID 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wex 1492  wcel 2148  wne 2347  wral 2455  {crab 2459  Vcvv 2737  cin 3128  c0 3422  {csn 3591  {cpr 3592   class class class wbr 4000  Tr wtr 4098  Ord word 4359  Oncon0 4360  ωcom 4586  1oc1o 6404  2oc2o 6405  cen 6732  Fincfn 6734
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-in1 614  ax-in2 615  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-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-1o 6411  df-2o 6412  df-er 6529  df-en 6735  df-fin 6737
This theorem is referenced by:  exmidonfin  7187
  Copyright terms: Public domain W3C validator