Theorem naddelim

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑏 = 𝐴 → ( 𝑏 +no 𝐶 ) = ( 𝐴 +no 𝐶 ) )
2	1	eleq1d	⊢ ( 𝑏 = 𝐴 → ( ( 𝑏 +no 𝐶 ) ∈ 𝑥 ↔ ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
3	2	rspcv	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 → ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
4	3	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 → ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
5	4	adantld	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) → ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
6	5	ralrimiva	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑥 ∈ On ( ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) → ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
7		ovex	⊢ ( 𝐴 +no 𝐶 ) ∈ V
8	7	elintrab	⊢ ( ( 𝐴 +no 𝐶 ) ∈ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } ↔ ∀ 𝑥 ∈ On ( ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) → ( 𝐴 +no 𝐶 ) ∈ 𝑥 ) )
9	6 8	sylibr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 +no 𝐶 ) ∈ ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } )
10		naddov2	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } )
11	10	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 +no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐵 +no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ 𝐶 ( 𝐵 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝑏 +no 𝐶 ) ∈ 𝑥 ) } )
13	9 12	eleqtrrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) )
14	13	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 +no 𝐶 ) ∈ ( 𝐵 +no 𝐶 ) ) )