Metamath Proof Explorer


Theorem naddel2

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

Ref Expression
Assertion naddel2 Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +no A ) e. ( C +no B ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 naddel1 Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( A +no C ) e. ( B +no C ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( A +no C ) e. ( B +no C ) ) ) with typecode |-
2 naddcom Could not format ( ( A e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) ) : No typesetting found for |- ( ( A e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) ) with typecode |-
3 2 3adant2 Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A +no C ) = ( C +no A ) ) with typecode |-
4 naddcom Could not format ( ( B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) : No typesetting found for |- ( ( B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) with typecode |-
5 4 3adant1 Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( B +no C ) = ( C +no B ) ) with typecode |-
6 3 5 eleq12d Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) e. ( B +no C ) <-> ( C +no A ) e. ( C +no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no C ) e. ( B +no C ) <-> ( C +no A ) e. ( C +no B ) ) ) with typecode |-
7 1 6 bitrd Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +no A ) e. ( C +no B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +no A ) e. ( C +no B ) ) ) with typecode |-