Metamath Proof Explorer


Theorem rankelun

Description: Rank membership is inherited by union. (Contributed by NM, 18-Sep-2006) (Proof shortened by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses rankelun.1 𝐴 ∈ V
rankelun.2 𝐵 ∈ V
rankelun.3 𝐶 ∈ V
rankelun.4 𝐷 ∈ V
Assertion rankelun ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ ( 𝐴𝐵 ) ) ∈ ( rank ‘ ( 𝐶𝐷 ) ) )

Proof

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 ‘ ( 𝐶𝐷 ) ) )