| Step | Hyp | Ref
| Expression |
| 1 | | brdomi 8999 |
. . . . 5
⊢ (𝐴 ≼ ω →
∃𝑓 𝑓:𝐴–1-1→ω) |
| 2 | 1 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω) → ∃𝑓 𝑓:𝐴–1-1→ω) |
| 3 | | reldom 8991 |
. . . . . 6
⊢ Rel
≼ |
| 4 | 3 | brrelex2i 5742 |
. . . . 5
⊢ (𝐴 ≼ ω → ω
∈ V) |
| 5 | | omelon2 7900 |
. . . . . . . . . . 11
⊢ (ω
∈ V → ω ∈ On) |
| 6 | 5 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → ω ∈
On) |
| 7 | | pwexg 5378 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ V) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → 𝒫 𝐴 ∈ V) |
| 9 | | inex1g 5319 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 𝐴 ∩ Fin) ∈ V) |
| 11 | | difss 4136 |
. . . . . . . . . . . 12
⊢
((𝒫 𝐴 ∩
Fin) ∖ {∅}) ⊆ (𝒫 𝐴 ∩ Fin) |
| 12 | | ssdomg 9040 |
. . . . . . . . . . . 12
⊢
((𝒫 𝐴 ∩
Fin) ∈ V → (((𝒫 𝐴 ∩ Fin) ∖ {∅}) ⊆
(𝒫 𝐴 ∩ Fin)
→ ((𝒫 𝐴 ∩
Fin) ∖ {∅}) ≼ (𝒫 𝐴 ∩ Fin))) |
| 13 | 10, 11, 12 | mpisyl 21 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ≼
(𝒫 𝐴 ∩
Fin)) |
| 14 | | f1f1orn 6859 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–1-1→ω → 𝑓:𝐴–1-1-onto→ran
𝑓) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → 𝑓:𝐴–1-1-onto→ran
𝑓) |
| 16 | | f1opwfi 9396 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1-onto→ran
𝑓 → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑓 “ 𝑥)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 ran 𝑓 ∩ Fin)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑓 “ 𝑥)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 ran 𝑓 ∩ Fin)) |
| 18 | | f1oeng 9011 |
. . . . . . . . . . . . 13
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ (𝑓 “
𝑥)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 ran 𝑓 ∩ Fin)) → (𝒫 𝐴 ∩ Fin) ≈ (𝒫
ran 𝑓 ∩
Fin)) |
| 19 | 10, 17, 18 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 𝐴 ∩ Fin) ≈ (𝒫 ran 𝑓 ∩ Fin)) |
| 20 | | pwexg 5378 |
. . . . . . . . . . . . . . . 16
⊢ (ω
∈ V → 𝒫 ω ∈ V) |
| 21 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → 𝒫 ω ∈
V) |
| 22 | | inex1g 5319 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 ω ∈ V → (𝒫 ω ∩ Fin) ∈
V) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 ω ∩ Fin)
∈ V) |
| 24 | | f1f 6804 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:𝐴–1-1→ω → 𝑓:𝐴⟶ω) |
| 25 | 24 | frnd 6744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1→ω → ran 𝑓 ⊆ ω) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → ran 𝑓 ⊆ ω) |
| 27 | 26 | sspwd 4613 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → 𝒫 ran 𝑓 ⊆ 𝒫
ω) |
| 28 | 27 | ssrind 4244 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 ran 𝑓 ∩ Fin) ⊆ (𝒫
ω ∩ Fin)) |
| 29 | | ssdomg 9040 |
. . . . . . . . . . . . . 14
⊢
((𝒫 ω ∩ Fin) ∈ V → ((𝒫 ran 𝑓 ∩ Fin) ⊆ (𝒫
ω ∩ Fin) → (𝒫 ran 𝑓 ∩ Fin) ≼ (𝒫 ω ∩
Fin))) |
| 30 | 23, 28, 29 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 ran 𝑓 ∩ Fin) ≼ (𝒫
ω ∩ Fin)) |
| 31 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑧 → {𝑓} = {𝑧}) |
| 32 | | pweq 4614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑧 → 𝒫 𝑓 = 𝒫 𝑧) |
| 33 | 31, 32 | xpeq12d 5716 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑧 → ({𝑓} × 𝒫 𝑓) = ({𝑧} × 𝒫 𝑧)) |
| 34 | 33 | cbviunv 5040 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓) = ∪ 𝑧 ∈ 𝑥 ({𝑧} × 𝒫 𝑧) |
| 35 | | iuneq1 5008 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ∪
𝑧 ∈ 𝑥 ({𝑧} × 𝒫 𝑧) = ∪ 𝑧 ∈ 𝑦 ({𝑧} × 𝒫 𝑧)) |
| 36 | 34, 35 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ∪
𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓) = ∪ 𝑧 ∈ 𝑦 ({𝑧} × 𝒫 𝑧)) |
| 37 | 36 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (card‘∪ 𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓)) = (card‘∪ 𝑧 ∈ 𝑦 ({𝑧} × 𝒫 𝑧))) |
| 38 | 37 | cbvmptv 5255 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓))) = (𝑦 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑧 ∈ 𝑦 ({𝑧} × 𝒫 𝑧))) |
| 39 | 38 | ackbij1 10277 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 ω ∩
Fin) ↦ (card‘∪ 𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓))):(𝒫 ω ∩ Fin)–1-1-onto→ω |
| 40 | | f1oeng 9011 |
. . . . . . . . . . . . . 14
⊢
(((𝒫 ω ∩ Fin) ∈ V ∧ (𝑥 ∈ (𝒫 ω ∩ Fin) ↦
(card‘∪ 𝑓 ∈ 𝑥 ({𝑓} × 𝒫 𝑓))):(𝒫 ω ∩ Fin)–1-1-onto→ω) → (𝒫 ω ∩ Fin)
≈ ω) |
| 41 | 23, 39, 40 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 ω ∩ Fin)
≈ ω) |
| 42 | | domentr 9053 |
. . . . . . . . . . . . 13
⊢
(((𝒫 ran 𝑓
∩ Fin) ≼ (𝒫 ω ∩ Fin) ∧ (𝒫 ω ∩
Fin) ≈ ω) → (𝒫 ran 𝑓 ∩ Fin) ≼ ω) |
| 43 | 30, 41, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 ran 𝑓 ∩ Fin) ≼
ω) |
| 44 | | endomtr 9052 |
. . . . . . . . . . . 12
⊢
(((𝒫 𝐴 ∩
Fin) ≈ (𝒫 ran 𝑓 ∩ Fin) ∧ (𝒫 ran 𝑓 ∩ Fin) ≼ ω)
→ (𝒫 𝐴 ∩
Fin) ≼ ω) |
| 45 | 19, 43, 44 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝒫 𝐴 ∩ Fin) ≼
ω) |
| 46 | | domtr 9047 |
. . . . . . . . . . 11
⊢
((((𝒫 𝐴
∩ Fin) ∖ {∅}) ≼ (𝒫 𝐴 ∩ Fin) ∧ (𝒫 𝐴 ∩ Fin) ≼ ω)
→ ((𝒫 𝐴 ∩
Fin) ∖ {∅}) ≼ ω) |
| 47 | 13, 45, 46 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ≼
ω) |
| 48 | | ondomen 10077 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ≼
ω) → ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∈ dom
card) |
| 49 | 6, 47, 48 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ∈ dom
card) |
| 50 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅})
↦ ∩ 𝑦) = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) |
| 51 | 50 | fifo 9472 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦):((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) |
| 52 | 51 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦):((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) |
| 53 | | fodomnum 10097 |
. . . . . . . . 9
⊢
(((𝒫 𝐴 ∩
Fin) ∖ {∅}) ∈ dom card → ((𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦):((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴) → (fi‘𝐴) ≼ ((𝒫 𝐴 ∩ Fin) ∖
{∅}))) |
| 54 | 49, 52, 53 | sylc 65 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (fi‘𝐴) ≼ ((𝒫 𝐴 ∩ Fin) ∖
{∅})) |
| 55 | | domtr 9047 |
. . . . . . . 8
⊢
(((fi‘𝐴)
≼ ((𝒫 𝐴 ∩
Fin) ∖ {∅}) ∧ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ≼
ω) → (fi‘𝐴) ≼ ω) |
| 56 | 54, 47, 55 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ ω ∈ V) ∧ 𝑓:𝐴–1-1→ω) → (fi‘𝐴) ≼ ω) |
| 57 | 56 | ex 412 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐵 ∧ ω ∈ V) → (𝑓:𝐴–1-1→ω → (fi‘𝐴) ≼ ω)) |
| 58 | 57 | exlimdv 1933 |
. . . . 5
⊢ ((𝐴 ∈ 𝐵 ∧ ω ∈ V) →
(∃𝑓 𝑓:𝐴–1-1→ω → (fi‘𝐴) ≼ ω)) |
| 59 | 4, 58 | sylan2 593 |
. . . 4
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω) → (∃𝑓 𝑓:𝐴–1-1→ω → (fi‘𝐴) ≼ ω)) |
| 60 | 2, 59 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω) → (fi‘𝐴) ≼
ω) |
| 61 | 60 | ex 412 |
. 2
⊢ (𝐴 ∈ 𝐵 → (𝐴 ≼ ω → (fi‘𝐴) ≼
ω)) |
| 62 | | fvex 6919 |
. . . 4
⊢
(fi‘𝐴) ∈
V |
| 63 | | ssfii 9459 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ (fi‘𝐴)) |
| 64 | | ssdomg 9040 |
. . . 4
⊢
((fi‘𝐴) ∈
V → (𝐴 ⊆
(fi‘𝐴) → 𝐴 ≼ (fi‘𝐴))) |
| 65 | 62, 63, 64 | mpsyl 68 |
. . 3
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≼ (fi‘𝐴)) |
| 66 | | domtr 9047 |
. . . 4
⊢ ((𝐴 ≼ (fi‘𝐴) ∧ (fi‘𝐴) ≼ ω) → 𝐴 ≼
ω) |
| 67 | 66 | ex 412 |
. . 3
⊢ (𝐴 ≼ (fi‘𝐴) → ((fi‘𝐴) ≼ ω → 𝐴 ≼
ω)) |
| 68 | 65, 67 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝐵 → ((fi‘𝐴) ≼ ω → 𝐴 ≼ ω)) |
| 69 | 61, 68 | impbid 212 |
1
⊢ (𝐴 ∈ 𝐵 → (𝐴 ≼ ω ↔ (fi‘𝐴) ≼
ω)) |