This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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