Theorem alephval2

Description: An alternate way to express the value of the aleph function for nonzero arguments. Theorem 64 of Suppes p. 229. (Contributed by NM, 15-Nov-2003)

	Ref	Expression
Assertion	alephval2	|- ( ( A e. On /\ (/) e. A ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } )

Proof

Step	Hyp	Ref	Expression
1		alephordi	|- ( A e. On -> ( y e. A -> ( aleph ` y ) ~< ( aleph ` A ) ) )
2	1	ralrimiv	|- ( A e. On -> A. y e. A ( aleph ` y ) ~< ( aleph ` A ) )
3		alephon	|- ( aleph ` A ) e. On
4	2 3	jctil	|- ( A e. On -> ( ( aleph ` A ) e. On /\ A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
5		breq2	|- ( x = ( aleph ` A ) -> ( ( aleph ` y ) ~< x <-> ( aleph ` y ) ~< ( aleph ` A ) ) )
6	5	ralbidv	|- ( x = ( aleph ` A ) -> ( A. y e. A ( aleph ` y ) ~< x <-> A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
7	6	elrab	|- ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } <-> ( ( aleph ` A ) e. On /\ A. y e. A ( aleph ` y ) ~< ( aleph ` A ) ) )
8	4 7	sylibr	|- ( A e. On -> ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
9		cardsdomelir	|- ( z e. ( card ` ( aleph ` A ) ) -> z ~< ( aleph ` A ) )
10		alephcard	|- ( card ` ( aleph ` A ) ) = ( aleph ` A )
11	10	eqcomi	|- ( aleph ` A ) = ( card ` ( aleph ` A ) )
12	9 11	eleq2s	|- ( z e. ( aleph ` A ) -> z ~< ( aleph ` A ) )
13		omex	|- _om e. _V
14		vex	|- z e. _V
15		entri3	|- ( ( _om e. _V /\ z e. _V ) -> ( _om ~<_ z \/ z ~<_ _om ) )
16	13 14 15	mp2an	|- ( _om ~<_ z \/ z ~<_ _om )
17		carddom	|- ( ( _om e. _V /\ z e. _V ) -> ( ( card ` _om ) C_ ( card ` z ) <-> _om ~<_ z ) )
18	13 14 17	mp2an	|- ( ( card ` _om ) C_ ( card ` z ) <-> _om ~<_ z )
19		cardom	|- ( card ` _om ) = _om
20	19	sseq1i	|- ( ( card ` _om ) C_ ( card ` z ) <-> _om C_ ( card ` z ) )
21	18 20	bitr3i	|- ( _om ~<_ z <-> _om C_ ( card ` z ) )
22		cardidm	|- ( card ` ( card ` z ) ) = ( card ` z )
23		cardalephex	|- ( _om C_ ( card ` z ) -> ( ( card ` ( card ` z ) ) = ( card ` z ) <-> E. x e. On ( card ` z ) = ( aleph ` x ) ) )
24	22 23	mpbii	|- ( _om C_ ( card ` z ) -> E. x e. On ( card ` z ) = ( aleph ` x ) )
25		alephord	|- ( ( x e. On /\ A e. On ) -> ( x e. A <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
26	25	ancoms	|- ( ( A e. On /\ x e. On ) -> ( x e. A <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
27		breq1	|- ( ( card ` z ) = ( aleph ` x ) -> ( ( card ` z ) ~< ( aleph ` A ) <-> ( aleph ` x ) ~< ( aleph ` A ) ) )
28	14	cardid	|- ( card ` z ) ~~ z
29		sdomen1	|- ( ( card ` z ) ~~ z -> ( ( card ` z ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) ) )
30	28 29	ax-mp	|- ( ( card ` z ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) )
31	27 30	bitr3di	|- ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< ( aleph ` A ) <-> z ~< ( aleph ` A ) ) )
32	26 31	sylan9bb	|- ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( x e. A <-> z ~< ( aleph ` A ) ) )
33		fveq2	|- ( y = x -> ( aleph ` y ) = ( aleph ` x ) )
34	33	breq1d	|- ( y = x -> ( ( aleph ` y ) ~< z <-> ( aleph ` x ) ~< z ) )
35	34	rspcv	|- ( x e. A -> ( A. y e. A ( aleph ` y ) ~< z -> ( aleph ` x ) ~< z ) )
36		sdomirr	|- -. ( aleph ` x ) ~< ( aleph ` x )
37		sdomen2	|- ( ( card ` z ) ~~ z -> ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< z ) )
38	28 37	ax-mp	|- ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< z )
39		breq2	|- ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< ( card ` z ) <-> ( aleph ` x ) ~< ( aleph ` x ) ) )
40	38 39	bitr3id	|- ( ( card ` z ) = ( aleph ` x ) -> ( ( aleph ` x ) ~< z <-> ( aleph ` x ) ~< ( aleph ` x ) ) )
41	36 40	mtbiri	|- ( ( card ` z ) = ( aleph ` x ) -> -. ( aleph ` x ) ~< z )
42	35 41	nsyli	|- ( x e. A -> ( ( card ` z ) = ( aleph ` x ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
43	42	com12	|- ( ( card ` z ) = ( aleph ` x ) -> ( x e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
44	43	adantl	|- ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( x e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
45	32 44	sylbird	|- ( ( ( A e. On /\ x e. On ) /\ ( card ` z ) = ( aleph ` x ) ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
46	45	rexlimdva2	|- ( A e. On -> ( E. x e. On ( card ` z ) = ( aleph ` x ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
47	24 46	syl5	|- ( A e. On -> ( _om C_ ( card ` z ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
48	21 47	syl5bi	|- ( A e. On -> ( _om ~<_ z -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
49	48	adantr	|- ( ( A e. On /\ (/) e. A ) -> ( _om ~<_ z -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
50		ne0i	|- ( (/) e. A -> A =/= (/) )
51		onelon	|- ( ( A e. On /\ y e. A ) -> y e. On )
52		alephgeom	|- ( y e. On <-> _om C_ ( aleph ` y ) )
53		alephon	|- ( aleph ` y ) e. On
54		ssdomg	|- ( ( aleph ` y ) e. On -> ( _om C_ ( aleph ` y ) -> _om ~<_ ( aleph ` y ) ) )
55	53 54	ax-mp	|- ( _om C_ ( aleph ` y ) -> _om ~<_ ( aleph ` y ) )
56	52 55	sylbi	|- ( y e. On -> _om ~<_ ( aleph ` y ) )
57		domtr	|- ( ( z ~<_ _om /\ _om ~<_ ( aleph ` y ) ) -> z ~<_ ( aleph ` y ) )
58	56 57	sylan2	|- ( ( z ~<_ _om /\ y e. On ) -> z ~<_ ( aleph ` y ) )
59		domnsym	|- ( z ~<_ ( aleph ` y ) -> -. ( aleph ` y ) ~< z )
60	58 59	syl	|- ( ( z ~<_ _om /\ y e. On ) -> -. ( aleph ` y ) ~< z )
61	51 60	sylan2	|- ( ( z ~<_ _om /\ ( A e. On /\ y e. A ) ) -> -. ( aleph ` y ) ~< z )
62	61	expr	|- ( ( z ~<_ _om /\ A e. On ) -> ( y e. A -> -. ( aleph ` y ) ~< z ) )
63	62	ralrimiv	|- ( ( z ~<_ _om /\ A e. On ) -> A. y e. A -. ( aleph ` y ) ~< z )
64		r19.2z	|- ( ( A =/= (/) /\ A. y e. A -. ( aleph ` y ) ~< z ) -> E. y e. A -. ( aleph ` y ) ~< z )
65	64	ex	|- ( A =/= (/) -> ( A. y e. A -. ( aleph ` y ) ~< z -> E. y e. A -. ( aleph ` y ) ~< z ) )
66	50 63 65	syl2im	|- ( (/) e. A -> ( ( z ~<_ _om /\ A e. On ) -> E. y e. A -. ( aleph ` y ) ~< z ) )
67		rexnal	|- ( E. y e. A -. ( aleph ` y ) ~< z <-> -. A. y e. A ( aleph ` y ) ~< z )
68	66 67	syl6ib	|- ( (/) e. A -> ( ( z ~<_ _om /\ A e. On ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
69	68	com12	|- ( ( z ~<_ _om /\ A e. On ) -> ( (/) e. A -> -. A. y e. A ( aleph ` y ) ~< z ) )
70	69	expimpd	|- ( z ~<_ _om -> ( ( A e. On /\ (/) e. A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
71	70	a1d	|- ( z ~<_ _om -> ( z ~< ( aleph ` A ) -> ( ( A e. On /\ (/) e. A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
72	71	com3r	|- ( ( A e. On /\ (/) e. A ) -> ( z ~<_ _om -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
73	49 72	jaod	|- ( ( A e. On /\ (/) e. A ) -> ( ( _om ~<_ z \/ z ~<_ _om ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) ) )
74	16 73	mpi	|- ( ( A e. On /\ (/) e. A ) -> ( z ~< ( aleph ` A ) -> -. A. y e. A ( aleph ` y ) ~< z ) )
75		breq2	|- ( x = z -> ( ( aleph ` y ) ~< x <-> ( aleph ` y ) ~< z ) )
76	75	ralbidv	|- ( x = z -> ( A. y e. A ( aleph ` y ) ~< x <-> A. y e. A ( aleph ` y ) ~< z ) )
77	76	elrab	|- ( z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } <-> ( z e. On /\ A. y e. A ( aleph ` y ) ~< z ) )
78	77	simprbi	|- ( z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } -> A. y e. A ( aleph ` y ) ~< z )
79	78	con3i	|- ( -. A. y e. A ( aleph ` y ) ~< z -> -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
80	12 74 79	syl56	|- ( ( A e. On /\ (/) e. A ) -> ( z e. ( aleph ` A ) -> -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) )
81	80	ralrimiv	|- ( ( A e. On /\ (/) e. A ) -> A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } )
82		ssrab2	|- { x e. On | A. y e. A ( aleph ` y ) ~< x } C_ On
83		oneqmini	|- ( { x e. On | A. y e. A ( aleph ` y ) ~< x } C_ On -> ( ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } /\ A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } ) )
84	82 83	ax-mp	|- ( ( ( aleph ` A ) e. { x e. On | A. y e. A ( aleph ` y ) ~< x } /\ A. z e. ( aleph ` A ) -. z e. { x e. On | A. y e. A ( aleph ` y ) ~< x } ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } )
85	8 81 84	syl2an2r	|- ( ( A e. On /\ (/) e. A ) -> ( aleph ` A ) = |^| { x e. On | A. y e. A ( aleph ` y ) ~< x } )