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 ‘ 𝑌 ) )