Theorem naddel12

Description: Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025)

	Ref	Expression
Assertion	naddel12	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐶 +no 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simprr	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐵 ∈ 𝐷 )
2		onelon	⊢ ( ( 𝐷 ∈ On ∧ 𝐵 ∈ 𝐷 ) → 𝐵 ∈ On )
3	2	ad2ant2l	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐵 ∈ On )
4		simplr	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐷 ∈ On )
5		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ On )
6	5	ad2ant2r	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐴 ∈ On )
7		naddel2	⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐷 ↔ ( 𝐴 +no 𝐵 ) ∈ ( 𝐴 +no 𝐷 ) ) )
8	3 4 6 7	syl3anc	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐵 ∈ 𝐷 ↔ ( 𝐴 +no 𝐵 ) ∈ ( 𝐴 +no 𝐷 ) ) )
9	1 8	mpbid	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐴 +no 𝐷 ) )
10		simprl	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐴 ∈ 𝐶 )
11		simpll	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → 𝐶 ∈ On )
12		naddel1	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 +no 𝐷 ) ∈ ( 𝐶 +no 𝐷 ) ) )
13	6 11 4 12	syl3anc	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 +no 𝐷 ) ∈ ( 𝐶 +no 𝐷 ) ) )
14	10 13	mpbid	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 +no 𝐷 ) ∈ ( 𝐶 +no 𝐷 ) )
15		naddcl	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +no 𝐷 ) ∈ On )
16	15	adantr	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐶 +no 𝐷 ) ∈ On )
17		ontr1	⊢ ( ( 𝐶 +no 𝐷 ) ∈ On → ( ( ( 𝐴 +no 𝐵 ) ∈ ( 𝐴 +no 𝐷 ) ∧ ( 𝐴 +no 𝐷 ) ∈ ( 𝐶 +no 𝐷 ) ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐶 +no 𝐷 ) ) )
18	16 17	syl	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( ( ( 𝐴 +no 𝐵 ) ∈ ( 𝐴 +no 𝐷 ) ∧ ( 𝐴 +no 𝐷 ) ∈ ( 𝐶 +no 𝐷 ) ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐶 +no 𝐷 ) ) )
19	9 14 18	mp2and	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐶 +no 𝐷 ) )
20	19	ex	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +no 𝐵 ) ∈ ( 𝐶 +no 𝐷 ) ) )