Metamath Proof Explorer


Theorem smoel2

Description: A strictly monotone ordinal function preserves the membership relation. (Contributed by Mario Carneiro, 12-Mar-2013)

Ref Expression
Assertion smoel2 FFnASmoFBACBFCFB

Proof

Step Hyp Ref Expression
1 fndm FFnAdomF=A
2 1 eleq2d FFnABdomFBA
3 2 anbi1d FFnABdomFCBBACB
4 3 biimprd FFnABACBBdomFCB
5 smoel SmoFBdomFCBFCFB
6 5 3expib SmoFBdomFCBFCFB
7 4 6 sylan9 FFnASmoFBACBFCFB
8 7 imp FFnASmoFBACBFCFB