Theorem smoel2

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

	Ref	Expression
Assertion	smoel2	|- ( ( ( F Fn A /\ Smo F ) /\ ( B e. A /\ C e. B ) ) -> ( F ` C ) e. ( F ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fndm	|- ( F Fn A -> dom F = A )
2	1	eleq2d	|- ( F Fn A -> ( B e. dom F <-> B e. A ) )
3	2	anbi1d	|- ( F Fn A -> ( ( B e. dom F /\ C e. B ) <-> ( B e. A /\ C e. B ) ) )
4	3	biimprd	|- ( F Fn A -> ( ( B e. A /\ C e. B ) -> ( B e. dom F /\ C e. B ) ) )
5		smoel	|- ( ( Smo F /\ B e. dom F /\ C e. B ) -> ( F ` C ) e. ( F ` B ) )
6	5	3expib	|- ( Smo F -> ( ( B e. dom F /\ C e. B ) -> ( F ` C ) e. ( F ` B ) ) )
7	4 6	sylan9	|- ( ( F Fn A /\ Smo F ) -> ( ( B e. A /\ C e. B ) -> ( F ` C ) e. ( F ` B ) ) )
8	7	imp	|- ( ( ( F Fn A /\ Smo F ) /\ ( B e. A /\ C e. B ) ) -> ( F ` C ) e. ( F ` B ) )