This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 onsuc 
 |-  ( 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 } )