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 \land Smo F) \land (B \in A \land C \in B)) \to F (C) \in F (B)$

Step	Hyp	Ref	Expression
1		fndm	$⊢ F Fn A \to dom F = A$
2	1	eleq2d	$⊢ F Fn A \to (B \in dom F \leftrightarrow B \in A)$
3	2	anbi1d	$⊢ F Fn A \to ((B \in dom F \land C \in B) \leftrightarrow (B \in A \land C \in B))$
4	3	biimprd	$⊢ F Fn A \to ((B \in A \land C \in B) \to (B \in dom F \land C \in B))$
5		smoel	$⊢ (Smo F \land B \in dom F \land C \in B) \to F (C) \in F (B)$
6	5	3expib	$⊢ Smo F \to ((B \in dom F \land C \in B) \to F (C) \in F (B))$
7	4 6	sylan9	$⊢ (F Fn A \land Smo F) \to ((B \in A \land C \in B) \to F (C) \in F (B))$
8	7	imp	$⊢ ((F Fn A \land Smo F) \land (B \in A \land C \in B)) \to F (C) \in F (B)$

Metamath Proof Explorer