Step | Hyp | Ref
| Expression |
1 | | relsdom 8897 |
. . 3
⊢ Rel
≺ |
2 | 1 | brrelex2i 5694 |
. 2
⊢ (𝐴 ≺ ω → ω
∈ V) |
3 | | sdomdom 8927 |
. . . 4
⊢ (𝐴 ≺ ω → 𝐴 ≼
ω) |
4 | | domeng 8909 |
. . . 4
⊢ (ω
∈ V → (𝐴 ≼
ω ↔ ∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω))) |
5 | 3, 4 | imbitrid 243 |
. . 3
⊢ (ω
∈ V → (𝐴 ≺
ω → ∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω))) |
6 | | ensym 8950 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ 𝑦 → 𝑦 ≈ 𝐴) |
7 | 6 | ad2antrl 727 |
. . . . . . . . . 10
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ≈ 𝐴) |
8 | | simpl 484 |
. . . . . . . . . 10
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ≺ ω) |
9 | | ensdomtr 9064 |
. . . . . . . . . 10
⊢ ((𝑦 ≈ 𝐴 ∧ 𝐴 ≺ ω) → 𝑦 ≺ ω) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . . . 9
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ≺ ω) |
11 | | sdomnen 8928 |
. . . . . . . . 9
⊢ (𝑦 ≺ ω → ¬
𝑦 ≈
ω) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → ¬ 𝑦 ≈
ω) |
13 | | simpr 486 |
. . . . . . . . 9
⊢ ((𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝑦 ⊆ ω) |
14 | | unbnn 9250 |
. . . . . . . . . 10
⊢ ((ω
∈ V ∧ 𝑦 ⊆
ω ∧ ∀𝑧
∈ ω ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤) → 𝑦 ≈ ω) |
15 | 14 | 3expia 1122 |
. . . . . . . . 9
⊢ ((ω
∈ V ∧ 𝑦 ⊆
ω) → (∀𝑧
∈ ω ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω)) |
16 | 2, 13, 15 | syl2an 597 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → (∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ≈ ω)) |
17 | 12, 16 | mtod 197 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → ¬ ∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
18 | | rexnal 3104 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
ω ¬ ∃𝑤
∈ 𝑦 𝑧 ∈ 𝑤 ↔ ¬ ∀𝑧 ∈ ω ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
19 | | omsson 7811 |
. . . . . . . . . . . . 13
⊢ ω
⊆ On |
20 | | sstr 3957 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ ω ∧ ω
⊆ On) → 𝑦
⊆ On) |
21 | 19, 20 | mpan2 690 |
. . . . . . . . . . . 12
⊢ (𝑦 ⊆ ω → 𝑦 ⊆ On) |
22 | | nnord 7815 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω → Ord 𝑧) |
23 | | ssel2 3944 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ On) |
24 | | vex 3452 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
25 | 24 | elon 6331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ On ↔ Ord 𝑤) |
26 | 23, 25 | sylib 217 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) → Ord 𝑤) |
27 | | ordtri1 6355 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝑤 ∧ Ord 𝑧) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
28 | 26, 27 | sylan 581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ⊆ On ∧ 𝑤 ∈ 𝑦) ∧ Ord 𝑧) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
29 | 28 | an32s 651 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ⊆ On ∧ Ord 𝑧) ∧ 𝑤 ∈ 𝑦) → (𝑤 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑤)) |
30 | 29 | ralbidva 3173 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∀𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧 ↔ ∀𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤)) |
31 | | unissb 4905 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦
⊆ 𝑧 ↔
∀𝑤 ∈ 𝑦 𝑤 ⊆ 𝑧) |
32 | | ralnex 3076 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑦 ¬ 𝑧 ∈ 𝑤 ↔ ¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤) |
33 | 32 | bicomi 223 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ ∀𝑤 ∈ 𝑦 ¬ 𝑧 ∈ 𝑤) |
34 | 30, 31, 33 | 3bitr4g 314 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∪ 𝑦
⊆ 𝑧 ↔ ¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤)) |
35 | | ordunisssuc 6428 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (∪ 𝑦
⊆ 𝑧 ↔ 𝑦 ⊆ suc 𝑧)) |
36 | 34, 35 | bitr3d 281 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ On ∧ Ord 𝑧) → (¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧)) |
37 | 21, 22, 36 | syl2an 597 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 ↔ 𝑦 ⊆ suc 𝑧)) |
38 | | peano2b 7824 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ω ↔ suc 𝑧 ∈
ω) |
39 | | ssnnfi 9120 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑧 ∈ ω ∧
𝑦 ⊆ suc 𝑧) → 𝑦 ∈ Fin) |
40 | 38, 39 | sylanb 582 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ω ∧ 𝑦 ⊆ suc 𝑧) → 𝑦 ∈ Fin) |
41 | 40 | ex 414 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω → (𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin)) |
42 | 41 | adantl 483 |
. . . . . . . . . . 11
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (𝑦 ⊆ suc 𝑧 → 𝑦 ∈ Fin)) |
43 | 37, 42 | sylbid 239 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ ω ∧ 𝑧 ∈ ω) → (¬
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
44 | 43 | rexlimdva 3153 |
. . . . . . . . 9
⊢ (𝑦 ⊆ ω →
(∃𝑧 ∈ ω
¬ ∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
45 | 18, 44 | biimtrrid 242 |
. . . . . . . 8
⊢ (𝑦 ⊆ ω → (¬
∀𝑧 ∈ ω
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
46 | 45 | ad2antll 728 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → (¬
∀𝑧 ∈ ω
∃𝑤 ∈ 𝑦 𝑧 ∈ 𝑤 → 𝑦 ∈ Fin)) |
47 | 17, 46 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝑦 ∈ Fin) |
48 | | simprl 770 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ≈ 𝑦) |
49 | | enfii 9140 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝐴 ≈ 𝑦) → 𝐴 ∈ Fin) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . 5
⊢ ((𝐴 ≺ ω ∧ (𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω)) → 𝐴 ∈ Fin) |
51 | 50 | ex 414 |
. . . 4
⊢ (𝐴 ≺ ω → ((𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝐴 ∈ Fin)) |
52 | 51 | exlimdv 1937 |
. . 3
⊢ (𝐴 ≺ ω →
(∃𝑦(𝐴 ≈ 𝑦 ∧ 𝑦 ⊆ ω) → 𝐴 ∈ Fin)) |
53 | 5, 52 | sylcom 30 |
. 2
⊢ (ω
∈ V → (𝐴 ≺
ω → 𝐴 ∈
Fin)) |
54 | 2, 53 | mpcom 38 |
1
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |