Metamath Proof Explorer

Theorem naddel1

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

Ref Expression
Assertion naddel1 ⊢A∈On∧B∈On∧C∈On→A∈B↔A+C∈B+C

Proof

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