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

Theorem exmidonfinlem 7187
Description: Lemma for exmidonfin 7188. (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 3615 . . . . . . . . . 10 (𝑟 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2 exmidonfinlem.a . . . . . . . . . 10 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
31, 2eleq2s 2272 . . . . . . . . 9 (𝑟𝐴 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
4 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
54biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
6 elrabi 2890 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {∅})
7 velsn 3609 . . . . . . . . . . . . . 14 (𝑠 ∈ {∅} ↔ 𝑠 = ∅)
86, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = ∅)
9 biidd 172 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (𝜑𝜑))
109elrab 2893 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (𝑠 ∈ {∅} ∧ 𝜑))
1110simprbi 275 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
1211notnotd 630 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ ¬ 𝜑)
13 0ex 4128 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
1413snm 3712 . . . . . . . . . . . . . . . 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 4186 . . . . . . . . . . . . . . 15 {∅} ∈ V
2221rabex 4145 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V
2322prid2 3699 . . . . . . . . . . . . 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 4145 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ 𝜑} ∈ V
4140prid1 3698 . . . . . . . . . . . . 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 4102 . . . . . . 7 (Tr 𝐴 ↔ ∀𝑟𝐴𝑠𝑟 𝑠𝐴)
4947, 48mpbir 146 . . . . . 6 Tr 𝐴
50 elpri 3615 . . . . . . . . 9 (𝑧 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5150, 2eleq2s 2272 . . . . . . . 8 (𝑧𝐴 → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
52 ordtriexmidlem 4516 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ 𝜑} ∈ On
5352ontrci 4425 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ 𝜑}
54 treq 4105 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ 𝜑}))
5553, 54mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → Tr 𝑧)
56 ordtriexmidlem 4516 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ On
5756ontrci 4425 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}
58 treq 4105 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5957, 58mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → Tr 𝑧)
6055, 59jaoi 716 . . . . . . . 8 ((𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → Tr 𝑧)
6151, 60syl 14 . . . . . . 7 (𝑧𝐴 → Tr 𝑧)
6261rgen 2530 . . . . . 6 𝑧𝐴 Tr 𝑧
63 dford3 4365 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑧𝐴 Tr 𝑧))
6449, 62, 63mpbir2an 942 . . . . 5 Ord 𝐴
65 prexg 4209 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V)
6640, 22, 65mp2an 426 . . . . . . 7 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V
672, 66eqeltri 2250 . . . . . 6 𝐴 ∈ V
6867elon 4372 . . . . 5 (𝐴 ∈ On ↔ Ord 𝐴)
6964, 68mpbir 146 . . . 4 𝐴 ∈ On
70 2onn 6517 . . . . . 6 2o ∈ ω
71 nnfi 6867 . . . . . 6 (2o ∈ ω → 2o ∈ Fin)
7270, 71ax-mp 5 . . . . 5 2o ∈ Fin
73 pm5.19 706 . . . . . . . . . 10 ¬ (𝜑 ↔ ¬ 𝜑)
7413snm 3712 . . . . . . . . . . 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 7186 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
8240, 22, 81mp2an 426 . . . . . . 7 ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
8380, 82mpbir 146 . . . . . 6 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o
842, 83eqbrtri 4022 . . . . 5 𝐴 ≈ 2o
85 enfii 6869 . . . . 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 6425 . . . . 5 1o = {∅}
91 1lt2o 6438 . . . . 5 1o ∈ 2o
9290, 91eqeltrri 2251 . . . 4 {∅} ∈ 2o
93 nneneq 6852 . . . . . 6 ((𝐴 ∈ ω ∧ 2o ∈ ω) → (𝐴 ≈ 2o𝐴 = 2o))
9470, 93mpan2 425 . . . . 5 (𝐴 ∈ ω → (𝐴 ≈ 2o𝐴 = 2o))
9584, 94mpbii 148 . . . 4 (𝐴 ∈ ω → 𝐴 = 2o)
9692, 95eleqtrrid 2267 . . 3 (𝐴 ∈ ω → {∅} ∈ 𝐴)
97 elpri 3615 . . . 4 ({∅} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9897, 2eleq2s 2272 . . 3 ({∅} ∈ 𝐴 → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9996, 98syl 14 . 2 (𝐴 ∈ ω → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
10013snid 3623 . . . . . . 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 3592  {cpr 3593   class class class wbr 4001  Tr wtr 4099  Ord word 4360  Oncon0 4361  ωcom 4587  1oc1o 6405  2oc2o 6406  cen 6733  Fincfn 6735
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 4119  ax-nul 4127  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-iinf 4585
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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-br 4002  df-opab 4063  df-tr 4100  df-id 4291  df-iord 4364  df-on 4366  df-suc 4369  df-iom 4588  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-f1 5218  df-fo 5219  df-f1o 5220  df-fv 5221  df-1o 6412  df-2o 6413  df-er 6530  df-en 6736  df-fin 6738
This theorem is referenced by:  exmidonfin  7188
  Copyright terms: Public domain W3C validator