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

Theorem exmidonfinlem 7194
Description: Lemma for exmidonfin 7195. (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 3617 . . . . . . . . . 10 (𝑟 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2 exmidonfinlem.a . . . . . . . . . 10 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
31, 2eleq2s 2272 . . . . . . . . 9 (𝑟𝐴 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
4 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
54biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
6 elrabi 2892 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 ∈ {∅})
7 velsn 3611 . . . . . . . . . . . . . 14 (𝑠 ∈ {∅} ↔ 𝑠 = ∅)
86, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = ∅)
9 biidd 172 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑠 → (𝜑𝜑))
109elrab 2895 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (𝑠 ∈ {∅} ∧ 𝜑))
1110simprbi 275 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
1211notnotd 630 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ ¬ 𝜑)
13 0ex 4132 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
1413snm 3714 . . . . . . . . . . . . . . . 16 𝑤 𝑤 ∈ {∅}
15 r19.3rmv 3515 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑))
1614, 15ax-mp 5 . . . . . . . . . . . . . . 15 (¬ ¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1712, 16sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
18 rabeq0 3454 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ ¬ 𝜑)
1917, 18sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → {𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅)
208, 19eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
21 p0ex 4190 . . . . . . . . . . . . . . 15 {∅} ∈ V
2221rabex 4149 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V
2322prid2 3701 . . . . . . . . . . . . 13 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}
2423, 2eleqtrri 2253 . . . . . . . . . . . 12 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ 𝐴
2520, 24eqeltrdi 2268 . . . . . . . . . . 11 (𝑠 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴)
265, 25syl6 33 . . . . . . . . . 10 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ 𝜑} → 𝑠𝐴))
27 eleq2 2241 . . . . . . . . . . . 12 (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (𝑠𝑟𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
2827biimpcd 159 . . . . . . . . . . 11 (𝑠𝑟 → (𝑟 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
29 elrabi 2892 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 ∈ {∅})
3029, 7sylib 122 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = ∅)
31 biidd 172 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑠 → (¬ 𝜑 ↔ ¬ 𝜑))
3231elrab 2895 . . . . . . . . . . . . . . . 16 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ↔ (𝑠 ∈ {∅} ∧ ¬ 𝜑))
3332simprbi 275 . . . . . . . . . . . . . . 15 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ¬ 𝜑)
34 r19.3rmv 3515 . . . . . . . . . . . . . . . 16 (∃𝑤 𝑤 ∈ {∅} → (¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑))
3514, 34ax-mp 5 . . . . . . . . . . . . . . 15 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3633, 35sylib 122 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∀𝑥 ∈ {∅} ¬ 𝜑)
37 rabeq0 3454 . . . . . . . . . . . . . 14 ({𝑥 ∈ {∅} ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ {∅} ¬ 𝜑)
3836, 37sylibr 134 . . . . . . . . . . . . 13 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → {𝑥 ∈ {∅} ∣ 𝜑} = ∅)
3930, 38eqtr4d 2213 . . . . . . . . . . . 12 (𝑠 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → 𝑠 = {𝑥 ∈ {∅} ∣ 𝜑})
4021rabex 4149 . . . . . . . . . . . . . 14 {𝑥 ∈ {∅} ∣ 𝜑} ∈ V
4140prid1 3700 . . . . . . . . . . . . 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 4106 . . . . . . 7 (Tr 𝐴 ↔ ∀𝑟𝐴𝑠𝑟 𝑠𝐴)
4947, 48mpbir 146 . . . . . 6 Tr 𝐴
50 elpri 3617 . . . . . . . . 9 (𝑧 ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5150, 2eleq2s 2272 . . . . . . . 8 (𝑧𝐴 → (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
52 ordtriexmidlem 4520 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ 𝜑} ∈ On
5352ontrci 4429 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ 𝜑}
54 treq 4109 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ 𝜑}))
5553, 54mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} → Tr 𝑧)
56 ordtriexmidlem 4520 . . . . . . . . . . 11 {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ On
5756ontrci 4429 . . . . . . . . . 10 Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}
58 treq 4109 . . . . . . . . . 10 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (Tr 𝑧 ↔ Tr {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
5957, 58mpbiri 168 . . . . . . . . 9 (𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → Tr 𝑧)
6055, 59jaoi 716 . . . . . . . 8 ((𝑧 = {𝑥 ∈ {∅} ∣ 𝜑} ∨ 𝑧 = {𝑥 ∈ {∅} ∣ ¬ 𝜑}) → Tr 𝑧)
6151, 60syl 14 . . . . . . 7 (𝑧𝐴 → Tr 𝑧)
6261rgen 2530 . . . . . 6 𝑧𝐴 Tr 𝑧
63 dford3 4369 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑧𝐴 Tr 𝑧))
6449, 62, 63mpbir2an 942 . . . . 5 Ord 𝐴
65 prexg 4213 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V)
6640, 22, 65mp2an 426 . . . . . . 7 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ∈ V
672, 66eqeltri 2250 . . . . . 6 𝐴 ∈ V
6867elon 4376 . . . . 5 (𝐴 ∈ On ↔ Ord 𝐴)
6964, 68mpbir 146 . . . 4 𝐴 ∈ On
70 2onn 6524 . . . . . 6 2o ∈ ω
71 nnfi 6874 . . . . . 6 (2o ∈ ω → 2o ∈ Fin)
7270, 71ax-mp 5 . . . . 5 2o ∈ Fin
73 pm5.19 706 . . . . . . . . . 10 ¬ (𝜑 ↔ ¬ 𝜑)
7413snm 3714 . . . . . . . . . . 11 𝑦 𝑦 ∈ {∅}
75 r19.3rmv 3515 . . . . . . . . . . 11 (∃𝑦 𝑦 ∈ {∅} → ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)))
7674, 75ax-mp 5 . . . . . . . . . 10 ((𝜑 ↔ ¬ 𝜑) ↔ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑))
7773, 76mtbi 670 . . . . . . . . 9 ¬ ∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑)
78 rabbi 2655 . . . . . . . . 9 (∀𝑥 ∈ {∅} (𝜑 ↔ ¬ 𝜑) ↔ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑})
7977, 78mtbi 670 . . . . . . . 8 ¬ {𝑥 ∈ {∅} ∣ 𝜑} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}
8079neir 2350 . . . . . . 7 {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}
81 pr2ne 7193 . . . . . . . 8 (({𝑥 ∈ {∅} ∣ 𝜑} ∈ V ∧ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ∈ V) → ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
8240, 22, 81mp2an 426 . . . . . . 7 ({{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o ↔ {𝑥 ∈ {∅} ∣ 𝜑} ≠ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
8380, 82mpbir 146 . . . . . 6 {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ≈ 2o
842, 83eqbrtri 4026 . . . . 5 𝐴 ≈ 2o
85 enfii 6876 . . . . 5 ((2o ∈ Fin ∧ 𝐴 ≈ 2o) → 𝐴 ∈ Fin)
8672, 84, 85mp2an 426 . . . 4 𝐴 ∈ Fin
8769, 86elini 3321 . . 3 𝐴 ∈ (On ∩ Fin)
88 eleq2 2241 . . 3 (ω = (On ∩ Fin) → (𝐴 ∈ ω ↔ 𝐴 ∈ (On ∩ Fin)))
8987, 88mpbiri 168 . 2 (ω = (On ∩ Fin) → 𝐴 ∈ ω)
90 df1o2 6432 . . . . 5 1o = {∅}
91 1lt2o 6445 . . . . 5 1o ∈ 2o
9290, 91eqeltrri 2251 . . . 4 {∅} ∈ 2o
93 nneneq 6859 . . . . . 6 ((𝐴 ∈ ω ∧ 2o ∈ ω) → (𝐴 ≈ 2o𝐴 = 2o))
9470, 93mpan2 425 . . . . 5 (𝐴 ∈ ω → (𝐴 ≈ 2o𝐴 = 2o))
9584, 94mpbii 148 . . . 4 (𝐴 ∈ ω → 𝐴 = 2o)
9692, 95eleqtrrid 2267 . . 3 (𝐴 ∈ ω → {∅} ∈ 𝐴)
97 elpri 3617 . . . 4 ({∅} ∈ {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9897, 2eleq2s 2272 . . 3 ({∅} ∈ 𝐴 → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
9996, 98syl 14 . 2 (𝐴 ∈ ω → ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
10013snid 3625 . . . . . . 7 ∅ ∈ {∅}
101 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑}))
102100, 101mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑})
103 biidd 172 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜑))
104103elrab 2895 . . . . . 6 (∅ ∈ {𝑥 ∈ {∅} ∣ 𝜑} ↔ (∅ ∈ {∅} ∧ 𝜑))
105102, 104sylib 122 . . . . 5 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → (∅ ∈ {∅} ∧ 𝜑))
106105simprd 114 . . . 4 ({∅} = {𝑥 ∈ {∅} ∣ 𝜑} → 𝜑)
107 eleq2 2241 . . . . . . 7 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (∅ ∈ {∅} ↔ ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑}))
108100, 107mpbii 148 . . . . . 6 ({∅} = {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ∅ ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑})
109 biidd 172 . . . . . . 7 (𝑥 = ∅ → (¬ 𝜑 ↔ ¬ 𝜑))
110109elrab 2895 . . . . . 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 2739  cin 3130  c0 3424  {csn 3594  {cpr 3595   class class class wbr 4005  Tr wtr 4103  Ord word 4364  Oncon0 4365  ωcom 4591  1oc1o 6412  2oc2o 6413  cen 6740  Fincfn 6742
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 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
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 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1o 6419  df-2o 6420  df-er 6537  df-en 6743  df-fin 6745
This theorem is referenced by:  exmidonfin  7195
  Copyright terms: Public domain W3C validator