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

Theorem exmidonfinlem 7192
Description: Lemma for exmidonfin 7193. (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 3616 . . . . . . . . . 10 (𝑟 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2 exmidonfinlem.a . . . . . . . . . 10 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
31, 2eleq2s 2272 . . . . . . . . 9 (𝑟𝐴 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
4 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
54biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
6 elrabi 2891 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {∅})
7 velsn 3610 . . . . . . . . . . . . . 14 (𝑠 ∈ {∅} ↔ 𝑠 = ∅)
86, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = ∅)
9 biidd 172 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (𝜑𝜑))
109elrab 2894 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (𝑠 ∈ {∅} ∧ 𝜑))
1110simprbi 275 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
1211notnotd 630 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ ¬ 𝜑)
13 0ex 4131 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
1413snm 3713 . . . . . . . . . . . . . . . 16 𝑤 𝑤 ∈ {∅}
15 r19.3rmv 3514 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑))
1614, 15ax-mp 5 . . . . . . . . . . . . . . 15 (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1712, 16sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
18 rabeq0 3453 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1917, 18sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → {𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅)
208, 19eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
21 p0ex 4189 . . . . . . . . . . . . . . 15 {∅} ∈ V
2221rabex 4148 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V
2322prid2 3700 . . . . . . . . . . . . 13 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
2423, 2eleqtrri 2253 . . . . . . . . . . . 12 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ 𝐴
2520, 24eqeltrdi 2268 . . . . . . . . . . 11 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴)
265, 25syl6 33 . . . . . . . . . 10 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴))
27 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2827biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
29 elrabi 2891 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {∅})
3029, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = ∅)
31 biidd 172 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (¬ 𝜑 ↔ ¬ 𝜑))
3231elrab 2894 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ↔ (𝑠 ∈ {∅} ∧ ¬ 𝜑))
3332simprbi 275 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ¬ 𝜑)
34 r19.3rmv 3514 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑))
3514, 34ax-mp 5 . . . . . . . . . . . . . . 15 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3633, 35sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∀𝑥 ∈ {∅} ¬ 𝜑)
37 rabeq0 3453 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3836, 37sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → {𝑥 ∈ {∅} ∣ 𝜑} = ∅)
3930, 38eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ 𝜑})
4021rabex 4148 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ 𝜑} ∈ V
4140prid1 3699 . . . . . . . . . . . . 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 4105 . . . . . . 7 (Tr 𝐴 ↔ ∀𝑟𝐴𝑠𝑟 𝑠𝐴)
4947, 48mpbir 146 . . . . . 6 Tr 𝐴
50 elpri 3616 . . . . . . . . 9 (𝑧 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5150, 2eleq2s 2272 . . . . . . . 8 (𝑧𝐴 → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
52 ordtriexmidlem 4519 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ 𝜑} ∈ On
5352ontrci 4428 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ 𝜑}
54 treq 4108 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ 𝜑}))
5553, 54mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → Tr 𝑧)
56 ordtriexmidlem 4519 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ On
5756ontrci 4428 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}
58 treq 4108 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5957, 58mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → Tr 𝑧)
6055, 59jaoi 716 . . . . . . . 8 ((𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → Tr 𝑧)
6151, 60syl 14 . . . . . . 7 (𝑧𝐴 → Tr 𝑧)
6261rgen 2530 . . . . . 6 𝑧𝐴 Tr 𝑧
63 dford3 4368 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑧𝐴 Tr 𝑧))
6449, 62, 63mpbir2an 942 . . . . 5 Ord 𝐴
65 prexg 4212 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V)
6640, 22, 65mp2an 426 . . . . . . 7 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V
672, 66eqeltri 2250 . . . . . 6 𝐴 ∈ V
6867elon 4375 . . . . 5 (𝐴 ∈ On ↔ Ord 𝐴)
6964, 68mpbir 146 . . . 4 𝐴 ∈ On
70 2onn 6522 . . . . . 6 2o ∈ ω
71 nnfi 6872 . . . . . 6 (2o ∈ ω → 2o ∈ Fin)
7270, 71ax-mp 5 . . . . 5 2o ∈ Fin
73 pm5.19 706 . . . . . . . . . 10 ¬ (𝜑 ↔ ¬ 𝜑)
7413snm 3713 . . . . . . . . . . 11 𝑦 𝑦 ∈ {∅}
75 r19.3rmv 3514 . . . . . . . . . . 11 (∃𝑦 𝑦 ∈ {∅} → ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)))
7674, 75ax-mp 5 . . . . . . . . . 10 ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑))
7773, 76mtbi 670 . . . . . . . . 9 ¬ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)
78 rabbi 2655 . . . . . . . . 9 (∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑) ↔ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
7977, 78mtbi 670 . . . . . . . 8 ¬ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}
8079neir 2350 . . . . . . 7 {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}
81 pr2ne 7191 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
8240, 22, 81mp2an 426 . . . . . . 7 ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
8380, 82mpbir 146 . . . . . 6 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o
842, 83eqbrtri 4025 . . . . 5 𝐴 ≈ 2o
85 enfii 6874 . . . . 5 ((2o ∈ Fin ∧ 𝐴 ≈ 2o) → 𝐴 ∈ Fin)
8672, 84, 85mp2an 426 . . . 4 𝐴 ∈ Fin
8769, 86elini 3320 . . 3 𝐴 ∈ (On ∩ Fin)
88 eleq2 2241 . . 3 (ω = (On ∩ Fin) → (𝐴 ∈ ω ↔ 𝐴 ∈ (On ∩ Fin)))
8987, 88mpbiri 168 . 2 (ω = (On ∩ Fin) → 𝐴 ∈ ω)
90 df1o2 6430 . . . . 5 1o = {∅}
91 1lt2o 6443 . . . . 5 1o ∈ 2o
9290, 91eqeltrri 2251 . . . 4 {∅} ∈ 2o
93 nneneq 6857 . . . . . 6 ((𝐴 ∈ ω ∧ 2o ∈ ω) → (𝐴 ≈ 2o𝐴 = 2o))
9470, 93mpan2 425 . . . . 5 (𝐴 ∈ ω → (𝐴 ≈ 2o𝐴 = 2o))
9584, 94mpbii 148 . . . 4 (𝐴 ∈ ω → 𝐴 = 2o)
9692, 95eleqtrrid 2267 . . 3 (𝐴 ∈ ω → {∅} ∈ 𝐴)
97 elpri 3616 . . . 4 ({∅} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9897, 2eleq2s 2272 . . 3 ({∅} ∈ 𝐴 → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9996, 98syl 14 . 2 (𝐴 ∈ ω → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
10013snid 3624 . . . . . . 7 ∅ ∈ {∅}
101 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
102100, 101mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑})
103 biidd 172 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜑))
104103elrab 2894 . . . . . 6 (∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (∅ ∈ {∅} ∧ 𝜑))
105102, 104sylib 122 . . . . 5 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ∧ 𝜑))
106105simprd 114 . . . 4 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
107 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
108100, 107mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
109 biidd 172 . . . . . . 7 (𝑥 = ∅ → (¬ 𝜑 ↔ ¬ 𝜑))
110109elrab 2894 . . . . . 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 2738  cin 3129  c0 3423  {csn 3593  {cpr 3594   class class class wbr 4004  Tr wtr 4102  Ord word 4363  Oncon0 4364  ωcom 4590  1oc1o 6410  2oc2o 6411  cen 6738  Fincfn 6740
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 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
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 2740  df-sbc 2964  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-1o 6417  df-2o 6418  df-er 6535  df-en 6741  df-fin 6743
This theorem is referenced by:  exmidonfin  7193
  Copyright terms: Public domain W3C validator