Step |
Hyp |
Ref |
Expression |
1 |
|
rankelun.1 |
⊢ 𝐴 ∈ V |
2 |
|
rankelun.2 |
⊢ 𝐵 ∈ V |
3 |
|
rankelun.3 |
⊢ 𝐶 ∈ V |
4 |
|
rankelun.4 |
⊢ 𝐷 ∈ V |
5 |
|
rankon |
⊢ ( rank ‘ 𝐶 ) ∈ On |
6 |
|
rankon |
⊢ ( rank ‘ 𝐷 ) ∈ On |
7 |
5 6
|
onun2i |
⊢ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ∈ On |
8 |
7
|
onordi |
⊢ Ord ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) |
9 |
|
elun1 |
⊢ ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) → ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) |
10 |
|
elun2 |
⊢ ( ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) → ( rank ‘ 𝐵 ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) |
11 |
|
ordunel |
⊢ ( ( Ord ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ∧ ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ∧ ( rank ‘ 𝐵 ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) |
12 |
8 9 10 11
|
mp3an3an |
⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) ) |
13 |
1 2
|
rankun |
⊢ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) |
14 |
3 4
|
rankun |
⊢ ( rank ‘ ( 𝐶 ∪ 𝐷 ) ) = ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) |
15 |
12 13 14
|
3eltr4g |
⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ( rank ‘ ( 𝐶 ∪ 𝐷 ) ) ) |