![]() |
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 4517 or weak linearity in ordsoexmid 4558) 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 2890 | . . . . . . . . 9 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑧 ∈ {∅}) | |
3 | velsn 3608 | . . . . . . . . 9 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅) | |
4 | 2, 3 | sylib 122 | . . . . . . . 8 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → 𝑧 = ∅) |
5 | noel 3426 | . . . . . . . . 9 ⊢ ¬ 𝑦 ∈ ∅ | |
6 | eleq2 2241 | . . . . . . . . 9 ⊢ (𝑧 = ∅ → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ∅)) | |
7 | 5, 6 | mtbiri 675 | . . . . . . . 8 ⊢ (𝑧 = ∅ → ¬ 𝑦 ∈ 𝑧) |
8 | 4, 7 | syl 14 | . . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑} → ¬ 𝑦 ∈ 𝑧) |
9 | 8 | adantl 277 | . . . . . 6 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → ¬ 𝑦 ∈ 𝑧) |
10 | 1, 9 | pm2.21dd 620 | . . . . 5 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) |
11 | 10 | gen2 1450 | . . . 4 ⊢ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) |
12 | dftr2 4100 | . . . 4 ⊢ (Tr {𝑥 ∈ {∅} ∣ 𝜑} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ {∅} ∣ 𝜑}) → 𝑦 ∈ {𝑥 ∈ {∅} ∣ 𝜑})) | |
13 | 11, 12 | mpbir 146 | . . 3 ⊢ Tr {𝑥 ∈ {∅} ∣ 𝜑} |
14 | ssrab2 3240 | . . 3 ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ⊆ {∅} | |
15 | ord0 4388 | . . . . 5 ⊢ Ord ∅ | |
16 | ordsucim 4496 | . . . . 5 ⊢ (Ord ∅ → Ord suc ∅) | |
17 | 15, 16 | ax-mp 5 | . . . 4 ⊢ Ord suc ∅ |
18 | suc0 4408 | . . . . 5 ⊢ suc ∅ = {∅} | |
19 | ordeq 4369 | . . . . 5 ⊢ (suc ∅ = {∅} → (Ord suc ∅ ↔ Ord {∅})) | |
20 | 18, 19 | ax-mp 5 | . . . 4 ⊢ (Ord suc ∅ ↔ Ord {∅}) |
21 | 17, 20 | mpbi 145 | . . 3 ⊢ Ord {∅} |
22 | trssord 4377 | . . 3 ⊢ ((Tr {𝑥 ∈ {∅} ∣ 𝜑} ∧ {𝑥 ∈ {∅} ∣ 𝜑} ⊆ {∅} ∧ Ord {∅}) → Ord {𝑥 ∈ {∅} ∣ 𝜑}) | |
23 | 13, 14, 21, 22 | mp3an 1337 | . 2 ⊢ Ord {𝑥 ∈ {∅} ∣ 𝜑} |
24 | p0ex 4185 | . . . 4 ⊢ {∅} ∈ V | |
25 | 24 | rabex 4144 | . . 3 ⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ V |
26 | 25 | elon 4371 | . 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 1351 = wceq 1353 ∈ wcel 2148 {crab 2459 ⊆ wss 3129 ∅c0 3422 {csn 3591 Tr wtr 4098 Ord word 4359 Oncon0 4360 suc csuc 4362 |
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-14 2151 ax-ext 2159 ax-sep 4118 ax-nul 4126 ax-pow 4171 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3576 df-sn 3597 df-uni 3808 df-tr 4099 df-iord 4363 df-on 4365 df-suc 4368 |
This theorem is referenced by: ordtriexmid 4517 ontriexmidim 4518 ordtri2orexmid 4519 ontr2exmid 4521 onsucsssucexmid 4523 ordsoexmid 4558 0elsucexmid 4561 ordpwsucexmid 4566 unfiexmid 6911 exmidonfinlem 7186 |
Copyright terms: Public domain | W3C validator |