Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (card‘𝑥) = (card‘𝑦)) |
2 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
3 | 1, 2 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((card‘𝑥) = 𝑥 ↔ (card‘𝑦) = 𝑦)) |
4 | 3 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (card‘𝑦) = 𝑦)) |
5 | | cardon 8653 |
. . . . . . . . 9
⊢
(card‘𝑦)
∈ On |
6 | | eleq1 2676 |
. . . . . . . . 9
⊢
((card‘𝑦) =
𝑦 → ((card‘𝑦) ∈ On ↔ 𝑦 ∈ On)) |
7 | 5, 6 | mpbii 222 |
. . . . . . . 8
⊢
((card‘𝑦) =
𝑦 → 𝑦 ∈ On) |
8 | 4, 7 | syl6com 36 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (card‘𝑥) = 𝑥 → (𝑦 ∈ 𝐴 → 𝑦 ∈ On)) |
9 | 8 | ssrdv 3574 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (card‘𝑥) = 𝑥 → 𝐴 ⊆ On) |
10 | | ssonuni 6878 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴
∈ On)) |
11 | 9, 10 | syl5 33 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → ∪ 𝐴 ∈ On)) |
12 | 11 | imp 444 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → ∪ 𝐴 ∈ On) |
13 | | cardonle 8666 |
. . . 4
⊢ (∪ 𝐴
∈ On → (card‘∪ 𝐴) ⊆ ∪ 𝐴) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → (card‘∪ 𝐴)
⊆ ∪ 𝐴) |
15 | | cardon 8653 |
. . . . 5
⊢
(card‘∪ 𝐴) ∈ On |
16 | 15 | onirri 5751 |
. . . 4
⊢ ¬
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴) |
17 | | eluni 4375 |
. . . . . . . 8
⊢
((card‘∪ 𝐴) ∈ ∪ 𝐴 ↔ ∃𝑦((card‘∪ 𝐴)
∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) |
18 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴) |
19 | | ssdomg 7887 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝐴
∈ On → (𝑦 ⊆
∪ 𝐴 → 𝑦 ≼ ∪ 𝐴)) |
20 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → (𝑦
⊆ ∪ 𝐴 → 𝑦 ≼ ∪ 𝐴)) |
21 | 18, 20 | syl5 33 |
. . . . . . . . . . . . . . . . 17
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → (𝑦 ∈
𝐴 → 𝑦 ≼ ∪ 𝐴)) |
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘𝑦) =
𝑦 → (card‘𝑦) = 𝑦) |
23 | | onenon 8658 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((card‘𝑦)
∈ On → (card‘𝑦) ∈ dom card) |
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(card‘𝑦)
∈ dom card |
25 | 22, 24 | syl6eqelr 2697 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝑦) =
𝑦 → 𝑦 ∈ dom card) |
26 | | onenon 8658 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝐴
∈ On → ∪ 𝐴 ∈ dom card) |
27 | | carddom2 8686 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ dom card ∧ ∪ 𝐴
∈ dom card) → ((card‘𝑦) ⊆ (card‘∪ 𝐴)
↔ 𝑦 ≼ ∪ 𝐴)) |
28 | 25, 26, 27 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → ((card‘𝑦) ⊆ (card‘∪ 𝐴)
↔ 𝑦 ≼ ∪ 𝐴)) |
29 | 21, 28 | sylibrd 248 |
. . . . . . . . . . . . . . . 16
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → (𝑦 ∈
𝐴 → (card‘𝑦) ⊆ (card‘∪ 𝐴))) |
30 | | sseq1 3589 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘𝑦) =
𝑦 → ((card‘𝑦) ⊆ (card‘∪ 𝐴)
↔ 𝑦 ⊆
(card‘∪ 𝐴))) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → ((card‘𝑦) ⊆ (card‘∪ 𝐴)
↔ 𝑦 ⊆
(card‘∪ 𝐴))) |
32 | 29, 31 | sylibd 228 |
. . . . . . . . . . . . . . 15
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → (𝑦 ∈
𝐴 → 𝑦 ⊆ (card‘∪ 𝐴))) |
33 | | ssel 3562 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ (card‘∪ 𝐴)
→ ((card‘∪ 𝐴) ∈ 𝑦 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴))) |
34 | 32, 33 | syl6 34 |
. . . . . . . . . . . . . 14
⊢
(((card‘𝑦) =
𝑦 ∧ ∪ 𝐴
∈ On) → (𝑦 ∈
𝐴 → ((card‘∪ 𝐴)
∈ 𝑦 →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴)))) |
35 | 34 | ex 449 |
. . . . . . . . . . . . 13
⊢
((card‘𝑦) =
𝑦 → (∪ 𝐴
∈ On → (𝑦 ∈
𝐴 → ((card‘∪ 𝐴)
∈ 𝑦 →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴))))) |
36 | 35 | com3r 85 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → ((card‘𝑦) = 𝑦 → (∪ 𝐴 ∈ On →
((card‘∪ 𝐴) ∈ 𝑦 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴))))) |
37 | 4, 36 | syld 46 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (∪ 𝐴 ∈ On →
((card‘∪ 𝐴) ∈ 𝑦 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴))))) |
38 | 37 | com4r 92 |
. . . . . . . . . 10
⊢
((card‘∪ 𝐴) ∈ 𝑦 → (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (∪ 𝐴 ∈ On →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴))))) |
39 | 38 | imp 444 |
. . . . . . . . 9
⊢
(((card‘∪ 𝐴) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (∪ 𝐴 ∈ On →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴)))) |
40 | 39 | exlimiv 1845 |
. . . . . . . 8
⊢
(∃𝑦((card‘∪
𝐴) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (∪ 𝐴 ∈ On →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴)))) |
41 | 17, 40 | sylbi 206 |
. . . . . . 7
⊢
((card‘∪ 𝐴) ∈ ∪ 𝐴 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (∪ 𝐴 ∈ On →
(card‘∪ 𝐴) ∈ (card‘∪ 𝐴)))) |
42 | 41 | com13 86 |
. . . . . 6
⊢ (∪ 𝐴
∈ On → (∀𝑥
∈ 𝐴 (card‘𝑥) = 𝑥 → ((card‘∪ 𝐴)
∈ ∪ 𝐴 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴)))) |
43 | 42 | imp 444 |
. . . . 5
⊢ ((∪ 𝐴
∈ On ∧ ∀𝑥
∈ 𝐴 (card‘𝑥) = 𝑥) → ((card‘∪ 𝐴)
∈ ∪ 𝐴 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴))) |
44 | 12, 43 | sylancom 698 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → ((card‘∪ 𝐴)
∈ ∪ 𝐴 → (card‘∪ 𝐴)
∈ (card‘∪ 𝐴))) |
45 | 16, 44 | mtoi 189 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → ¬ (card‘∪ 𝐴)
∈ ∪ 𝐴) |
46 | 15 | onordi 5749 |
. . . 4
⊢ Ord
(card‘∪ 𝐴) |
47 | | eloni 5650 |
. . . . 5
⊢ (∪ 𝐴
∈ On → Ord ∪ 𝐴) |
48 | 12, 47 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → Ord ∪
𝐴) |
49 | | ordtri4 5678 |
. . . 4
⊢ ((Ord
(card‘∪ 𝐴) ∧ Ord ∪
𝐴) →
((card‘∪ 𝐴) = ∪ 𝐴 ↔ ((card‘∪ 𝐴)
⊆ ∪ 𝐴 ∧ ¬ (card‘∪ 𝐴)
∈ ∪ 𝐴))) |
50 | 46, 48, 49 | sylancr 694 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → ((card‘∪ 𝐴) =
∪ 𝐴 ↔ ((card‘∪ 𝐴)
⊆ ∪ 𝐴 ∧ ¬ (card‘∪ 𝐴)
∈ ∪ 𝐴))) |
51 | 14, 45, 50 | mpbir2and 959 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥) → (card‘∪ 𝐴) =
∪ 𝐴) |
52 | 51 | ex 449 |
1
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (card‘∪ 𝐴) =
∪ 𝐴)) |