Theorem naddss1

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

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

Proof

Step	Hyp	Ref	Expression
1		naddel1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 +no 𝐶 ) ∈ ( 𝐴 +no 𝐶 ) ) )
2	1	3com12	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 +no 𝐶 ) ∈ ( 𝐴 +no 𝐶 ) ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ ( 𝐵 +no 𝐶 ) ∈ ( 𝐴 +no 𝐶 ) ) )
4		ontri1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
6		naddcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) ∈ On )
7	6	3adant2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) ∈ On )
8		naddcl	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On )
9	8	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On )
10		ontri1	⊢ ( ( ( 𝐴 +no 𝐶 ) ∈ On ∧ ( 𝐵 +no 𝐶 ) ∈ On ) → ( ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ↔ ¬ ( 𝐵 +no 𝐶 ) ∈ ( 𝐴 +no 𝐶 ) ) )
11	7 9 10	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ↔ ¬ ( 𝐵 +no 𝐶 ) ∈ ( 𝐴 +no 𝐶 ) ) )
12	3 5 11	3bitr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 +no 𝐶 ) ⊆ ( 𝐵 +no 𝐶 ) ) )