Step |
Hyp |
Ref |
Expression |
1 |
|
cardon |
⊢ ( card ‘ 𝐴 ) ∈ On |
2 |
|
cardon |
⊢ ( card ‘ 𝐵 ) ∈ On |
3 |
|
oacl |
⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On ) |
4 |
1 2 3
|
mp2an |
⊢ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On |
5 |
|
cardadju |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) |
6 |
5
|
ensymd |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) ) |
7 |
|
isnumi |
⊢ ( ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card ) |
8 |
4 6 7
|
sylancr |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card ) |