Step |
Hyp |
Ref |
Expression |
1 |
|
uniexg |
⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V ) |
2 |
|
ssorduni |
⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 ) |
3 |
|
elong |
⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) ) |
4 |
3
|
biimpar |
⊢ ( ( ∪ 𝐴 ∈ V ∧ Ord ∪ 𝐴 ) → ∪ 𝐴 ∈ On ) |
5 |
1 2 4
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → ∪ 𝐴 ∈ On ) |
6 |
|
suceloni |
⊢ ( ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ On ) |
7 |
|
onenon |
⊢ ( suc ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ dom card ) |
8 |
5 6 7
|
3syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → suc ∪ 𝐴 ∈ dom card ) |
9 |
|
onsucuni |
⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 ) |
10 |
9
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → 𝐴 ⊆ suc ∪ 𝐴 ) |
11 |
|
ssnum |
⊢ ( ( suc ∪ 𝐴 ∈ dom card ∧ 𝐴 ⊆ suc ∪ 𝐴 ) → 𝐴 ∈ dom card ) |
12 |
8 10 11
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → 𝐴 ∈ dom card ) |