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

Metamath Proof Explorer

Theorem harword

Description: Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Assertion harword ( 𝑋 ≼ 𝑌 → ( har ‘ 𝑋 ) ⊆ ( har ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 domtr ⊢ ( ( 𝑦 ≼ 𝑋 ∧ 𝑋 ≼ 𝑌 ) → 𝑦 ≼ 𝑌 )
2 1 expcom ⊢ ( 𝑋 ≼ 𝑌 → ( 𝑦 ≼ 𝑋 → 𝑦 ≼ 𝑌 ) )
3 2 adantr ⊢ ( ( 𝑋 ≼ 𝑌 ∧ 𝑦 ∈ On ) → ( 𝑦 ≼ 𝑋 → 𝑦 ≼ 𝑌 ) )
4 3 ss2rabdv ⊢ ( 𝑋 ≼ 𝑌 → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } ⊆ { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑌 } )
5 reldom ⊢ Rel ≼
6 5 brrelex1i ⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ∈ V )
7 harval ⊢ ( 𝑋 ∈ V → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )
8 6 7 syl ⊢ ( 𝑋 ≼ 𝑌 → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } )
9 5 brrelex2i ⊢ ( 𝑋 ≼ 𝑌 → 𝑌 ∈ V )
10 harval ⊢ ( 𝑌 ∈ V → ( har ‘ 𝑌 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑌 } )
11 9 10 syl ⊢ ( 𝑋 ≼ 𝑌 → ( har ‘ 𝑌 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑌 } )
12 4 8 11 3sstr4d ⊢ ( 𝑋 ≼ 𝑌 → ( har ‘ 𝑋 ) ⊆ ( har ‘ 𝑌 ) )