Theorem card2inf

Description: The alternate definition of the cardinal of a set given in cardval2 has the curious property that for non-numerable sets (for which ndmfv yields (/) ), it still evaluates to a nonempty set, and indeed it contains _om . (Contributed by Mario Carneiro, 15-Jan-2013) (Revised by Mario Carneiro, 27-Apr-2015)

	Ref	Expression
Hypothesis	card2inf.1	|- A e. _V
Assertion	card2inf	|- ( -. E. y e. On y ~~ A -> _om C_ { x e. On | x ~< A } )

Proof

Step	Hyp	Ref	Expression
1		card2inf.1	|- A e. _V
2		breq1	|- ( x = (/) -> ( x ~< A <-> (/) ~< A ) )
3		breq1	|- ( x = n -> ( x ~< A <-> n ~< A ) )
4		breq1	|- ( x = suc n -> ( x ~< A <-> suc n ~< A ) )
5		0elon	|- (/) e. On
6		breq1	|- ( y = (/) -> ( y ~~ A <-> (/) ~~ A ) )
7	6	rspcev	|- ( ( (/) e. On /\ (/) ~~ A ) -> E. y e. On y ~~ A )
8	5 7	mpan	|- ( (/) ~~ A -> E. y e. On y ~~ A )
9	8	con3i	|- ( -. E. y e. On y ~~ A -> -. (/) ~~ A )
10	1	0dom	|- (/) ~<_ A
11		brsdom	|- ( (/) ~< A <-> ( (/) ~<_ A /\ -. (/) ~~ A ) )
12	10 11	mpbiran	|- ( (/) ~< A <-> -. (/) ~~ A )
13	9 12	sylibr	|- ( -. E. y e. On y ~~ A -> (/) ~< A )
14		sucdom2	|- ( n ~< A -> suc n ~<_ A )
15	14	ad2antll	|- ( ( n e. _om /\ ( -. E. y e. On y ~~ A /\ n ~< A ) ) -> suc n ~<_ A )
16		nnon	|- ( n e. _om -> n e. On )
17		suceloni	|- ( n e. On -> suc n e. On )
18		breq1	|- ( y = suc n -> ( y ~~ A <-> suc n ~~ A ) )
19	18	rspcev	|- ( ( suc n e. On /\ suc n ~~ A ) -> E. y e. On y ~~ A )
20	19	ex	|- ( suc n e. On -> ( suc n ~~ A -> E. y e. On y ~~ A ) )
21	16 17 20	3syl	|- ( n e. _om -> ( suc n ~~ A -> E. y e. On y ~~ A ) )
22	21	con3dimp	|- ( ( n e. _om /\ -. E. y e. On y ~~ A ) -> -. suc n ~~ A )
23	22	adantrr	|- ( ( n e. _om /\ ( -. E. y e. On y ~~ A /\ n ~< A ) ) -> -. suc n ~~ A )
24		brsdom	|- ( suc n ~< A <-> ( suc n ~<_ A /\ -. suc n ~~ A ) )
25	15 23 24	sylanbrc	|- ( ( n e. _om /\ ( -. E. y e. On y ~~ A /\ n ~< A ) ) -> suc n ~< A )
26	25	exp32	|- ( n e. _om -> ( -. E. y e. On y ~~ A -> ( n ~< A -> suc n ~< A ) ) )
27	2 3 4 13 26	finds2	|- ( x e. _om -> ( -. E. y e. On y ~~ A -> x ~< A ) )
28	27	com12	|- ( -. E. y e. On y ~~ A -> ( x e. _om -> x ~< A ) )
29	28	ralrimiv	|- ( -. E. y e. On y ~~ A -> A. x e. _om x ~< A )
30		omsson	|- _om C_ On
31		ssrab	|- ( _om C_ { x e. On | x ~< A } <-> ( _om C_ On /\ A. x e. _om x ~< A ) )
32	30 31	mpbiran	|- ( _om C_ { x e. On | x ~< A } <-> A. x e. _om x ~< A )
33	29 32	sylibr	|- ( -. E. y e. On y ~~ A -> _om C_ { x e. On | x ~< A } )