![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ordtriexmidlem | GIF version |
Description: Lemma for decidability and ordinals. The set {𝑥 ∈ {∅} ∣ 𝜑} is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4553 or weak linearity in ordsoexmid 4594) with a proposition 𝜑. Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.) |
Ref | Expression |
---|---|
ordtriexmidlem | ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 109 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ 𝑧) | |
2 | elrabi 2913 | . . . . . . . . 9 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑧 ∈ {∅}) | |
3 | velsn 3635 | . . . . . . . . 9 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅) | |
4 | 2, 3 | sylib 122 | . . . . . . . 8 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑧 = ∅) |
5 | noel 3450 | . . . . . . . . 9 ⊢ ¬ 𝑦 ∈ ∅ | |
6 | eleq2 2257 | . . . . . . . . 9 ⊢ (𝑧 = ∅ → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ∅)) | |
7 | 5, 6 | mtbiri 676 | . . . . . . . 8 ⊢ (𝑧 = ∅ → ¬ 𝑦 ∈ 𝑧) |
8 | 4, 7 | syl 14 | . . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ 𝑦 ∈ 𝑧) |
9 | 8 | adantl 277 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → ¬ 𝑦 ∈ 𝑧) |
10 | 1, 9 | pm2.21dd 621 | . . . . 5 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) |
11 | 10 | gen2 1461 | . . . 4 ⊢ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) |
12 | dftr2 4129 | . . . 4 ⊢ (Tr {𝑥 ∈ {∅} ∣ 𝜑} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑})) | |
13 | 11, 12 | mpbir 146 | . . 3 ⊢ Tr {𝑥 ∈ {∅} ∣ 𝜑} |
14 | ssrab2 3264 | . . 3 ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ⊆ {∅} | |
15 | ord0 4422 | . . . . 5 ⊢ Ord ∅ | |
16 | ordsucim 4532 | . . . . 5 ⊢ (Ord ∅ → Ord suc ∅) | |
17 | 15, 16 | ax-mp 5 | . . . 4 ⊢ Ord suc ∅ |
18 | suc0 4442 | . . . . 5 ⊢ suc ∅ = {∅} | |
19 | ordeq 4403 | . . . . 5 ⊢ (suc ∅ = {∅} → (Ord suc ∅ ↔ Ord {∅})) | |
20 | 18, 19 | ax-mp 5 | . . . 4 ⊢ (Ord suc ∅ ↔ Ord {∅}) |
21 | 17, 20 | mpbi 145 | . . 3 ⊢ Ord {∅} |
22 | trssord 4411 | . . 3 ⊢ ((Tr {𝑥 ∈ {∅} ∣ 𝜑} ∧ {𝑥 ∈ {∅} ∣ 𝜑} ⊆ {∅} ∧ Ord {∅}) → Ord {𝑥 ∈ {∅} ∣ 𝜑}) | |
23 | 13, 14, 21, 22 | mp3an 1348 | . 2 ⊢ Ord {𝑥 ∈ {∅} ∣ 𝜑} |
24 | p0ex 4217 | . . . 4 ⊢ {∅} ∈ V | |
25 | 24 | rabex 4173 | . . 3 ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ V |
26 | 25 | elon 4405 | . 2 ⊢ ({𝑥 ∈ {∅} ∣ 𝜑} ∈ On ↔ Ord {𝑥 ∈ {∅} ∣ 𝜑}) |
27 | 23, 26 | mpbir 146 | 1 ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ On |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1362 = wceq 1364 ∈ wcel 2164 {crab 2476 ⊆ wss 3153 ∅c0 3446 {csn 3618 Tr wtr 4127 Ord word 4393 Oncon0 4394 suc csuc 4396 |
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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-nul 4155 ax-pow 4203 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-uni 3836 df-tr 4128 df-iord 4397 df-on 4399 df-suc 4402 |
This theorem is referenced by: ordtriexmid 4553 ontriexmidim 4554 ordtri2orexmid 4555 ontr2exmid 4557 onsucsssucexmid 4559 ordsoexmid 4594 0elsucexmid 4597 ordpwsucexmid 4602 unfiexmid 6974 exmidonfinlem 7253 |
Copyright terms: Public domain | W3C validator |