Metamath Proof Explorer


Theorem epelon2

Description: Over the ordinal numbers, one may define the relation A _E B iff A e. B and one finds that, under this ordering, On is a well-ordered class, see epweon . This is a weak form of epelg which only requires that we know B to be a set. (Contributed by RP, 27-Sep-2023)

Ref Expression
Assertion epelon2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 E 𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 epelg ( 𝐵 ∈ On → ( 𝐴 E 𝐵𝐴𝐵 ) )
2 1 adantl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 E 𝐵𝐴𝐵 ) )