Theorem smoel2

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

	Ref	Expression
Assertion	smoel2	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
2	1	eleq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴 ) )
3	2	anbi1d	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐵 ∈ dom 𝐹 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )
4	3	biimprd	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐵 ∈ dom 𝐹 ∧ 𝐶 ∈ 𝐵 ) ) )
5		smoel	⊢ ( ( Smo 𝐹 ∧ 𝐵 ∈ dom 𝐹 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) )
6	5	3expib	⊢ ( Smo 𝐹 → ( ( 𝐵 ∈ dom 𝐹 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) ) )
7	4 6	sylan9	⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) ) )
8	7	imp	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) )