Metamath Proof Explorer


Theorem naddss2

Description: Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024)

Ref Expression
Assertion naddss2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴𝐵 ↔ ( 𝐶 +no 𝐴 ) ⊆ ( 𝐶 +no 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 naddss1 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴𝐵 ↔ ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )
2 naddcom ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) = ( 𝐶 +no 𝐴 ) )
3 2 3adant2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) = ( 𝐶 +no 𝐴 ) )
4 naddcom ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
5 4 3adant1 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ( 𝐶 +no 𝐵 ) )
6 3 5 sseq12d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ↔ ( 𝐶 +no 𝐴 ) ⊆ ( 𝐶 +no 𝐵 ) ) )
7 1 6 bitrd ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴𝐵 ↔ ( 𝐶 +no 𝐴 ) ⊆ ( 𝐶 +no 𝐵 ) ) )