| Step | Hyp | Ref
| Expression |
| 1 | | relsdom 8992 |
. . 3
⊢ Rel
≺ |
| 2 | 1 | brrelex2i 5742 |
. 2
⊢ (𝐴 ≺ ω → ω
∈ V) |
| 3 | | sdomdom 9020 |
. . . 4
⊢ (𝐴 ≺ ω → 𝐴 ≼
ω) |
| 4 | | domeng 9003 |
. . . 4
⊢ (ω
∈ V → (𝐴 ≼
ω ↔ ∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω))) |
| 5 | 3, 4 | imbitrid 244 |
. . 3
⊢ (ω
∈ V → (𝐴 ≺
ω → ∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω))) |
| 6 | | ensym 9043 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ 𝑦 → 𝑦 ≈ 𝐴) |
| 7 | 6 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ≈ 𝐴) |
| 8 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ≺ ω) |
| 9 | | ensdomtr 9153 |
. . . . . . . . . 10
⊢ ((𝑦 ≈ 𝐴 ∧ 𝐴 ≺ ω) → 𝑦 ≺ ω) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ≺ ω) |
| 11 | | sdomnen 9021 |
. . . . . . . . 9
⊢ (𝑦 ≺ ω → ¬
𝑦 ≈
ω) |
| 12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → ¬ 𝑦 ≈
ω) |
| 13 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝑦 ⊆ ω) |
| 14 | | unbnn 9332 |
. . . . . . . . . 10
⊢ ((ω
∈ V ∧ 𝑦 ⊆
ω ∧ ∀𝑧
∈ ω ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤) → 𝑦 ≈ ω) |
| 15 | 14 | 3expia 1122 |
. . . . . . . . 9
⊢ ((ω
∈ V ∧ 𝑦 ⊆
ω) → (∀𝑧
∈ ω ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω)) |
| 16 | 2, 13, 15 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → (∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω)) |
| 17 | 12, 16 | mtod 198 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → ¬ ∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
| 18 | | rexnal 3100 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
ω ¬ ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤 ↔ ¬ ∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
| 19 | | omsson 7891 |
. . . . . . . . . . . . 13
⊢ ω
⊆ On |
| 20 | | sstr 3992 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ ω ∧ ω
⊆ On) → 𝑦
⊆ On) |
| 21 | 19, 20 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ω → 𝑦 ⊆ On) |
| 22 | | nnord 7895 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω → Ord 𝑧) |
| 23 | | ssel2 3978 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ On) |
| 24 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
| 25 | 24 | elon 6393 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ On ↔ Ord 𝑤) |
| 26 | 23, 25 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) → Ord 𝑤) |
| 27 | | ordtri1 6417 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝑤 ∧ Ord 𝑧) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
| 28 | 26, 27 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) ∧ Ord 𝑧) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
| 29 | 28 | an32s 652 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ⊆ On ∧ Ord 𝑧) ∧ 𝑤 ∈ 𝑦) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
| 30 | 29 | ralbidva 3176 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∀𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧 ↔ ∀𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤)) |
| 31 | | unissb 4939 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦
⊆ 𝑧 ↔
∀𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧) |
| 32 | | ralnex 3072 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑦 ¬ 𝑧 ∈ 𝑤 ↔ ¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
| 33 | 32 | bicomi 224 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ ∀𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤) |
| 34 | 30, 31, 33 | 3bitr4g 314 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∪ 𝑦
⊆ 𝑧 ↔ ¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤)) |
| 35 | | ordunisssuc 6490 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∪ 𝑦
⊆ 𝑧 ↔ 𝑦 ⊆ suc 𝑧)) |
| 36 | 34, 35 | bitr3d 281 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧)) |
| 37 | 21, 22, 36 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧)) |
| 38 | | peano2b 7904 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ω ↔ suc 𝑧 ∈
ω) |
| 39 | | ssnnfi 9209 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑧 ∈ ω ∧
𝑦 ⊆ suc 𝑧) → 𝑦 ∈ Fin) |
| 40 | 38, 39 | sylanb 581 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ω ∧ 𝑦 ⊆ suc 𝑧) → 𝑦 ∈ Fin) |
| 41 | 40 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω → (𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin)) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin)) |
| 43 | 37, 42 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
| 44 | 43 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (𝑦 ⊆ ω →
(∃𝑧 ∈ ω
¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
| 45 | 18, 44 | biimtrrid 243 |
. . . . . . . 8
⊢ (𝑦 ⊆ ω → (¬
∀𝑧 ∈ ω
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
| 46 | 45 | ad2antll 729 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → (¬
∀𝑧 ∈ ω
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
| 47 | 17, 46 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ∈ Fin) |
| 48 | | simprl 771 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ≈ 𝑦) |
| 49 | | enfii 9226 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝐴 ≈ 𝑦) → 𝐴 ∈ Fin) |
| 50 | 47, 48, 49 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ∈ Fin) |
| 51 | 50 | ex 412 |
. . . 4
⊢ (𝐴 ≺ ω → ((𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝐴 ∈ Fin)) |
| 52 | 51 | exlimdv 1933 |
. . 3
⊢ (𝐴 ≺ ω →
(∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝐴 ∈ Fin)) |
| 53 | 5, 52 | sylcom 30 |
. 2
⊢ (ω
∈ V → (𝐴 ≺
ω → 𝐴 ∈
Fin)) |
| 54 | 2, 53 | mpcom 38 |
1
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |