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

Metamath Proof Explorer

Theorem harval2

Description: An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harval2 ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )

Proof

Step Hyp Ref Expression
1 harval ⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝐴 } )
2 1 adantr ⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) → ( har ‘ 𝐴 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝐴 } )
3 sdomel ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ≺ 𝑥 → 𝑦 ∈ 𝑥 ) )
4 domsdomtr ⊢ ( ( 𝑦 ≼ 𝐴 ∧ 𝐴 ≺ 𝑥 ) → 𝑦 ≺ 𝑥 )
5 3 4 impel ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) ∧ ( 𝑦 ≼ 𝐴 ∧ 𝐴 ≺ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
6 5 an4s ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
7 6 ancoms ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ∧ ( 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) ) → 𝑦 ∈ 𝑥 )
8 7 3impb ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ∧ 𝑦 ∈ On ∧ 𝑦 ≼ 𝐴 ) → 𝑦 ∈ 𝑥 )
9 8 rabssdv ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝐴 } ⊆ 𝑥 )
10 9 adantl ⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) → { 𝑦 ∈ On ∣ 𝑦 ≼ 𝐴 } ⊆ 𝑥 )
11 2 10 eqsstrd ⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) → ( har ‘ 𝐴 ) ⊆ 𝑥 )
12 11 expr ⊢ ( ( 𝐴 ∈ dom card ∧ 𝑥 ∈ On ) → ( 𝐴 ≺ 𝑥 → ( har ‘ 𝐴 ) ⊆ 𝑥 ) )
13 12 ralrimiva ⊢ ( 𝐴 ∈ dom card → ∀ 𝑥 ∈ On ( 𝐴 ≺ 𝑥 → ( har ‘ 𝐴 ) ⊆ 𝑥 ) )
14 ssintrab ⊢ ( ( har ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ∀ 𝑥 ∈ On ( 𝐴 ≺ 𝑥 → ( har ‘ 𝐴 ) ⊆ 𝑥 ) )
15 13 14 sylibr ⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
16 breq2 ⊢ ( 𝑥 = ( har ‘ 𝐴 ) → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ( har ‘ 𝐴 ) ) )
17 harcl ⊢ ( har ‘ 𝐴 ) ∈ On
18 17 a1i ⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) ∈ On )
19 harsdom ⊢ ( 𝐴 ∈ dom card → 𝐴 ≺ ( har ‘ 𝐴 ) )
20 16 18 19 elrabd ⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
21 intss1 ⊢ ( ( har ‘ 𝐴 ) ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ ( har ‘ 𝐴 ) )
22 20 21 syl ⊢ ( 𝐴 ∈ dom card → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ ( har ‘ 𝐴 ) )
23 15 22 eqssd ⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )