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 ∣ 𝐴 ≺ 𝑥 } )