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	|- ( A e. dom card -> ( har ` A ) = |^| { x e. On | A ~< x } )

Proof

Step	Hyp	Ref	Expression
1		harval	|- ( A e. dom card -> ( har ` A ) = { y e. On | y ~<_ A } )
2	1	adantr	|- ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> ( har ` A ) = { y e. On | y ~<_ A } )
3		sdomel	|- ( ( y e. On /\ x e. On ) -> ( y ~< x -> y e. x ) )
4		domsdomtr	|- ( ( y ~<_ A /\ A ~< x ) -> y ~< x )
5	3 4	impel	|- ( ( ( y e. On /\ x e. On ) /\ ( y ~<_ A /\ A ~< x ) ) -> y e. x )
6	5	an4s	|- ( ( ( y e. On /\ y ~<_ A ) /\ ( x e. On /\ A ~< x ) ) -> y e. x )
7	6	ancoms	|- ( ( ( x e. On /\ A ~< x ) /\ ( y e. On /\ y ~<_ A ) ) -> y e. x )
8	7	3impb	|- ( ( ( x e. On /\ A ~< x ) /\ y e. On /\ y ~<_ A ) -> y e. x )
9	8	rabssdv	|- ( ( x e. On /\ A ~< x ) -> { y e. On | y ~<_ A } C_ x )
10	9	adantl	|- ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> { y e. On | y ~<_ A } C_ x )
11	2 10	eqsstrd	|- ( ( A e. dom card /\ ( x e. On /\ A ~< x ) ) -> ( har ` A ) C_ x )
12	11	expr	|- ( ( A e. dom card /\ x e. On ) -> ( A ~< x -> ( har ` A ) C_ x ) )
13	12	ralrimiva	|- ( A e. dom card -> A. x e. On ( A ~< x -> ( har ` A ) C_ x ) )
14		ssintrab	|- ( ( har ` A ) C_ |^| { x e. On | A ~< x } <-> A. x e. On ( A ~< x -> ( har ` A ) C_ x ) )
15	13 14	sylibr	|- ( A e. dom card -> ( har ` A ) C_ |^| { x e. On | A ~< x } )
16		breq2	|- ( x = ( har ` A ) -> ( A ~< x <-> A ~< ( har ` A ) ) )
17		harcl	|- ( har ` A ) e. On
18	17	a1i	|- ( A e. dom card -> ( har ` A ) e. On )
19		harsdom	|- ( A e. dom card -> A ~< ( har ` A ) )
20	16 18 19	elrabd	|- ( A e. dom card -> ( har ` A ) e. { x e. On | A ~< x } )
21		intss1	|- ( ( har ` A ) e. { x e. On | A ~< x } -> |^| { x e. On | A ~< x } C_ ( har ` A ) )
22	20 21	syl	|- ( A e. dom card -> |^| { x e. On | A ~< x } C_ ( har ` A ) )
23	15 22	eqssd	|- ( A e. dom card -> ( har ` A ) = |^| { x e. On | A ~< x } )