Metamath Proof Explorer

Theorem rankelop

Description: Rank membership is inherited by ordered pairs. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypotheses rankelun.1 ⊢ 𝐴 ∈ V
rankelun.2 ⊢ 𝐵 ∈ V
rankelun.3 ⊢ 𝐶 ∈ V
rankelun.4 ⊢ 𝐷 ∈ V
Assertion rankelop ( ( ( 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 1 2 3 4 rankelpr ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) ∈ ( rank ‘ { 𝐶 , 𝐷 } ) )
6 rankon ⊢ ( rank ‘ { 𝐶 , 𝐷 } ) ∈ On
7 6 onordi ⊢ Ord ( rank ‘ { 𝐶 , 𝐷 } )
8 ordsucelsuc ⊢ ( Ord ( rank ‘ { 𝐶 , 𝐷 } ) → ( ( rank ‘ { 𝐴 , 𝐵 } ) ∈ ( rank ‘ { 𝐶 , 𝐷 } ) ↔ suc ( rank ‘ { 𝐴 , 𝐵 } ) ∈ suc ( rank ‘ { 𝐶 , 𝐷 } ) ) )
9 7 8 ax-mp ⊢ ( ( rank ‘ { 𝐴 , 𝐵 } ) ∈ ( rank ‘ { 𝐶 , 𝐷 } ) ↔ suc ( rank ‘ { 𝐴 , 𝐵 } ) ∈ suc ( rank ‘ { 𝐶 , 𝐷 } ) )
10 5 9 sylib ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → suc ( rank ‘ { 𝐴 , 𝐵 } ) ∈ suc ( rank ‘ { 𝐶 , 𝐷 } ) )
11 1 2 rankop ⊢ ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
12 1 2 rankpr ⊢ ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
13 suceq ⊢ ( ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → suc ( rank ‘ { 𝐴 , 𝐵 } ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
14 12 13 ax-mp ⊢ suc ( rank ‘ { 𝐴 , 𝐵 } ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
15 11 14 eqtr4i ⊢ ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc ( rank ‘ { 𝐴 , 𝐵 } )
16 3 4 rankop ⊢ ( rank ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = suc suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
17 3 4 rankpr ⊢ ( rank ‘ { 𝐶 , 𝐷 } ) = suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
18 suceq ⊢ ( ( rank ‘ { 𝐶 , 𝐷 } ) = suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) → suc ( rank ‘ { 𝐶 , 𝐷 } ) = suc suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) ) )
19 17 18 ax-mp ⊢ suc ( rank ‘ { 𝐶 , 𝐷 } ) = suc suc ( ( rank ‘ 𝐶 ) ∪ ( rank ‘ 𝐷 ) )
20 16 19 eqtr4i ⊢ ( rank ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = suc ( rank ‘ { 𝐶 , 𝐷 } )
21 10 15 20 3eltr4g ⊢ ( ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐵 ) ∈ ( rank ‘ 𝐷 ) ) → ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( rank ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )