cardprclem

		Ref	Expression
	Hypothesis	cardprclem.1	\|- A = { x \| ( card ` x ) = x }
	Assertion	cardprclem	\|- -. A e. _V

Proof

Step	Hyp	Ref	Expression
1		cardprclem.1	\|- A = { x \| ( card ` x ) = x }
2	1	eleq2i	\|- ( x e. A <-> x e. { x \| ( card ` x ) = x } )
3		abid	\|- ( x e. { x \| ( card ` x ) = x } <-> ( card ` x ) = x )
4		iscard	\|- ( ( card ` x ) = x <-> ( x e. On /\ A. y e. x y ~< x ) )
5	2 3 4	3bitri	\|- ( x e. A <-> ( x e. On /\ A. y e. x y ~< x ) )
6	5	simplbi	\|- ( x e. A -> x e. On )
7	6	ssriv	\|- A C_ On
8		ssonuni	\|- ( A e. _V -> ( A C_ On -> U. A e. On ) )
9	7 8	mpi	\|- ( A e. _V -> U. A e. On )
10		domrefg	\|- ( U. A e. On -> U. A ~<_ U. A )
11	9 10	syl	\|- ( A e. _V -> U. A ~<_ U. A )
12		elharval	\|- ( U. A e. ( har ` U. A ) <-> ( U. A e. On /\ U. A ~<_ U. A ) )
13	9 11 12	sylanbrc	\|- ( A e. _V -> U. A e. ( har ` U. A ) )
14	7	sseli	\|- ( z e. A -> z e. On )
15		domrefg	\|- ( z e. On -> z ~<_ z )
16	15	ancli	\|- ( z e. On -> ( z e. On /\ z ~<_ z ) )
17		elharval	\|- ( z e. ( har ` z ) <-> ( z e. On /\ z ~<_ z ) )
18	16 17	sylibr	\|- ( z e. On -> z e. ( har ` z ) )
19	14 18	syl	\|- ( z e. A -> z e. ( har ` z ) )
20		harcard	\|- ( card ` ( har ` z ) ) = ( har ` z )
21		fvex	\|- ( har ` z ) e. _V
22		fveq2	\|- ( x = ( har ` z ) -> ( card ` x ) = ( card ` ( har ` z ) ) )
23		id	\|- ( x = ( har ` z ) -> x = ( har ` z ) )
24	22 23	eqeq12d	\|- ( x = ( har ` z ) -> ( ( card ` x ) = x <-> ( card ` ( har ` z ) ) = ( har ` z ) ) )
25	21 24 1	elab2	\|- ( ( har ` z ) e. A <-> ( card ` ( har ` z ) ) = ( har ` z ) )
26	20 25	mpbir	\|- ( har ` z ) e. A
27		eleq2	\|- ( w = ( har ` z ) -> ( z e. w <-> z e. ( har ` z ) ) )
28		eleq1	\|- ( w = ( har ` z ) -> ( w e. A <-> ( har ` z ) e. A ) )
29	27 28	anbi12d	\|- ( w = ( har ` z ) -> ( ( z e. w /\ w e. A ) <-> ( z e. ( har ` z ) /\ ( har ` z ) e. A ) ) )
30	21 29	spcev	\|- ( ( z e. ( har ` z ) /\ ( har ` z ) e. A ) -> E. w ( z e. w /\ w e. A ) )
31	19 26 30	sylancl	\|- ( z e. A -> E. w ( z e. w /\ w e. A ) )
32		eluni	\|- ( z e. U. A <-> E. w ( z e. w /\ w e. A ) )
33	31 32	sylibr	\|- ( z e. A -> z e. U. A )
34	33	ssriv	\|- A C_ U. A
35		harcard	\|- ( card ` ( har ` U. A ) ) = ( har ` U. A )
36		fvex	\|- ( har ` U. A ) e. _V
37		fveq2	\|- ( x = ( har ` U. A ) -> ( card ` x ) = ( card ` ( har ` U. A ) ) )
38		id	\|- ( x = ( har ` U. A ) -> x = ( har ` U. A ) )
39	37 38	eqeq12d	\|- ( x = ( har ` U. A ) -> ( ( card ` x ) = x <-> ( card ` ( har ` U. A ) ) = ( har ` U. A ) ) )
40	36 39 1	elab2	\|- ( ( har ` U. A ) e. A <-> ( card ` ( har ` U. A ) ) = ( har ` U. A ) )
41	35 40	mpbir	\|- ( har ` U. A ) e. A
42	34 41	sselii	\|- ( har ` U. A ) e. U. A
43	13 42	jctir	\|- ( A e. _V -> ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
44		eloni	\|- ( U. A e. On -> Ord U. A )
45		ordn2lp	\|- ( Ord U. A -> -. ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
46	9 44 45	3syl	\|- ( A e. _V -> -. ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
47	43 46	pm2.65i	\|- -. A e. _V

Metamath Proof Explorer

Theorem cardprclem

Proof