This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐹 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 𝐹 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐵 ) )