Theorem naddel1

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

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

Proof

Step	Hyp	Ref	Expression
1		naddelim	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )
2		naddssim	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ⊆ 𝐴 → ( 𝐵 +no 𝐶 ) ⊆ ( 𝐴 +no 𝐶 ) ) )
3	2	3com12	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ⊆ 𝐴 → ( 𝐵 +no 𝐶 ) ⊆ ( 𝐴 +no 𝐶 ) ) )
4		ontri1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
6	5	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
7		naddcl	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On )
8	7	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) ∈ On )
9		naddcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) ∈ On )
10		ontri1	⊢ ( ( ( 𝐵 +no 𝐶 ) ∈ On ∧ ( 𝐴 +no 𝐶 ) ∈ On ) → ( ( 𝐵 +no 𝐶 ) ⊆ ( 𝐴 +no 𝐶 ) ↔ ¬ ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )
11	8 9 10	3imp3i2an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐵 +no 𝐶 ) ⊆ ( 𝐴 +no 𝐶 ) ↔ ¬ ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )
12	3 6 11	3imtr3d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ 𝐴 ∈ 𝐵 → ¬ ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )
13	1 12	impcon4bid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )