| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . 3
⊢
(card‘𝐵)
∈ V |
| 2 | | ssid 4006 |
. . . . . . 7
⊢
(card‘𝐵)
⊆ (card‘𝐵) |
| 3 | | cfslb.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
| 4 | 3 | ssex 5321 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 → 𝐵 ∈ V) |
| 5 | 4 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → 𝐵 ∈ V) |
| 6 | | velpw 4605 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 7 | | sseq1 4009 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
| 8 | 6, 7 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
| 9 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ∪ 𝑥 = ∪
𝐵) |
| 10 | 9 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (∪ 𝑥 = 𝐴 ↔ ∪ 𝐵 = 𝐴)) |
| 11 | 8, 10 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ↔ (𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴))) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (card‘𝑥) = (card‘𝐵)) |
| 13 | 12 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((card‘𝑥) ⊆ (card‘𝐵) ↔ (card‘𝐵) ⊆ (card‘𝐵))) |
| 14 | 11, 13 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)))) |
| 15 | 14 | spcegv 3597 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))) |
| 16 | 5, 15 | mpcom 38 |
. . . . . . . 8
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
| 17 | | df-rex 3071 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
| 18 | | rabid 3458 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
| 19 | 18 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
| 20 | 19 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
| 21 | 17, 20 | bitri 275 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
| 22 | 16, 21 | sylibr 234 |
. . . . . . 7
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
| 23 | 2, 22 | mpan2 691 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
| 24 | | iinss 5056 |
. . . . . 6
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) → ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
| 25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → ∩
𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
| 26 | 3 | cflim3 10302 |
. . . . . 6
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) |
| 27 | 26 | sseq1d 4015 |
. . . . 5
⊢ (Lim
𝐴 → ((cf‘𝐴) ⊆ (card‘𝐵) ↔ ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))) |
| 28 | 25, 27 | imbitrrid 246 |
. . . 4
⊢ (Lim
𝐴 → ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵))) |
| 29 | 28 | 3impib 1117 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵)) |
| 30 | | ssdomg 9040 |
. . 3
⊢
((card‘𝐵)
∈ V → ((cf‘𝐴) ⊆ (card‘𝐵) → (cf‘𝐴) ≼ (card‘𝐵))) |
| 31 | 1, 29, 30 | mpsyl 68 |
. 2
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ (card‘𝐵)) |
| 32 | | limord 6444 |
. . . . . . 7
⊢ (Lim
𝐴 → Ord 𝐴) |
| 33 | | ordsson 7803 |
. . . . . . 7
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
| 34 | 32, 33 | syl 17 |
. . . . . 6
⊢ (Lim
𝐴 → 𝐴 ⊆ On) |
| 35 | | sstr2 3990 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ On → 𝐵 ⊆ On)) |
| 36 | 34, 35 | mpan9 506 |
. . . . 5
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ On) |
| 37 | | onssnum 10080 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐵 ⊆ On) → 𝐵 ∈ dom
card) |
| 38 | 4, 36, 37 | syl2an2 686 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) |
| 39 | | cardid2 9993 |
. . . 4
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
| 40 | 38, 39 | syl 17 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → (card‘𝐵) ≈ 𝐵) |
| 41 | 40 | 3adant3 1133 |
. 2
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (card‘𝐵) ≈ 𝐵) |
| 42 | | domentr 9053 |
. 2
⊢
(((cf‘𝐴)
≼ (card‘𝐵)
∧ (card‘𝐵)
≈ 𝐵) →
(cf‘𝐴) ≼ 𝐵) |
| 43 | 31, 41, 42 | syl2anc 584 |
1
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵) |