Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . 3
⊢
(card‘𝐵)
∈ V |
2 | | ssid 3624 |
. . . . . . 7
⊢
(card‘𝐵)
⊆ (card‘𝐵) |
3 | | cfslb.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
4 | 3 | ssex 4802 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 → 𝐵 ∈ V) |
5 | 4 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → 𝐵 ∈ V) |
6 | | selpw 4165 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
7 | | sseq1 3626 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
8 | 6, 7 | syl5bb 272 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
9 | | unieq 4444 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ∪ 𝑥 = ∪
𝐵) |
10 | 9 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (∪ 𝑥 = 𝐴 ↔ ∪ 𝐵 = 𝐴)) |
11 | 8, 10 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ↔ (𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴))) |
12 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (card‘𝑥) = (card‘𝐵)) |
13 | 12 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((card‘𝑥) ⊆ (card‘𝐵) ↔ (card‘𝐵) ⊆ (card‘𝐵))) |
14 | 11, 13 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)))) |
15 | 14 | spcegv 3294 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))) |
16 | 5, 15 | mpcom 38 |
. . . . . . . 8
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
17 | | df-rex 2918 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
18 | | rabid 3116 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
19 | 18 | anbi1i 731 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
20 | 19 | exbii 1774 |
. . . . . . . . 9
⊢
(∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
21 | 17, 20 | bitri 264 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))) |
22 | 16, 21 | sylibr 224 |
. . . . . . 7
⊢ (((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
23 | 2, 22 | mpan2 707 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
24 | | iinss 4571 |
. . . . . 6
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵) → ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → ∩
𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥) ⊆ (card‘𝐵)) |
26 | 3 | cflim3 9084 |
. . . . . 6
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) |
27 | 26 | sseq1d 3632 |
. . . . 5
⊢ (Lim
𝐴 → ((cf‘𝐴) ⊆ (card‘𝐵) ↔ ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))) |
28 | 25, 27 | syl5ibr 236 |
. . . 4
⊢ (Lim
𝐴 → ((𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵))) |
29 | 28 | 3impib 1262 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵)) |
30 | | ssdomg 8001 |
. . 3
⊢
((card‘𝐵)
∈ V → ((cf‘𝐴) ⊆ (card‘𝐵) → (cf‘𝐴) ≼ (card‘𝐵))) |
31 | 1, 29, 30 | mpsyl 68 |
. 2
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ (card‘𝐵)) |
32 | 4 | adantl 482 |
. . . . 5
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
33 | | limord 5784 |
. . . . . . 7
⊢ (Lim
𝐴 → Ord 𝐴) |
34 | | ordsson 6989 |
. . . . . . 7
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ (Lim
𝐴 → 𝐴 ⊆ On) |
36 | | sstr2 3610 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ On → 𝐵 ⊆ On)) |
37 | 35, 36 | mpan9 486 |
. . . . 5
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ On) |
38 | | onssnum 8863 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐵 ⊆ On) → 𝐵 ∈ dom
card) |
39 | 32, 37, 38 | syl2anc 693 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) |
40 | | cardid2 8779 |
. . . 4
⊢ (𝐵 ∈ dom card →
(card‘𝐵) ≈
𝐵) |
41 | 39, 40 | syl 17 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴) → (card‘𝐵) ≈ 𝐵) |
42 | 41 | 3adant3 1081 |
. 2
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (card‘𝐵) ≈ 𝐵) |
43 | | domentr 8015 |
. 2
⊢
(((cf‘𝐴)
≼ (card‘𝐵)
∧ (card‘𝐵)
≈ 𝐵) →
(cf‘𝐴) ≼ 𝐵) |
44 | 31, 42, 43 | syl2anc 693 |
1
⊢ ((Lim
𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵) |