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 ⊢ A ∈ V
rankelun.2 ⊢ B ∈ V
rankelun.3 ⊢ C ∈ V
rankelun.4 ⊢ D ∈ V
Assertion rankelun ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A ∪ B ∈ rank ⁡ C ∪ D

Proof

Step Hyp Ref Expression
1 rankelun.1 ⊢ A ∈ V
2 rankelun.2 ⊢ B ∈ V
3 rankelun.3 ⊢ C ∈ V
4 rankelun.4 ⊢ D ∈ V
5 rankon ⊢ rank ⁡ C ∈ On
6 rankon ⊢ rank ⁡ D ∈ On
7 5 6 onun2i ⊢ rank ⁡ C ∪ rank ⁡ D ∈ On
8 7 onordi ⊢ Ord ⁡ rank ⁡ C ∪ rank ⁡ D
9 elun1 ⊢ rank ⁡ A ∈ rank ⁡ C → rank ⁡ A ∈ rank ⁡ C ∪ rank ⁡ D
10 elun2 ⊢ rank ⁡ B ∈ rank ⁡ D → rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D
11 ordunel ⊢ Ord ⁡ rank ⁡ C ∪ rank ⁡ D ∧ rank ⁡ A ∈ rank ⁡ C ∪ rank ⁡ D ∧ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D → rank ⁡ A ∪ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D
12 8 9 10 11 mp3an3an ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A ∪ rank ⁡ B ∈ rank ⁡ C ∪ rank ⁡ D
13 1 2 rankun ⊢ rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B
14 3 4 rankun ⊢ rank ⁡ C ∪ D = rank ⁡ C ∪ rank ⁡ D
15 12 13 14 3eltr4g ⊢ rank ⁡ A ∈ rank ⁡ C ∧ rank ⁡ B ∈ rank ⁡ D → rank ⁡ A ∪ B ∈ rank ⁡ C ∪ D