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 V
Assertion card2inf ¬ y On y A ω x On | x A

Proof

Step Hyp Ref Expression
1 card2inf.1 A 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 On
6 breq1 y = y A A
7 6 rspcev On A y On y A
8 5 7 mpan A y On y A
9 8 con3i ¬ y On y A ¬ A
10 1 0dom A
11 brsdom A A ¬ A
12 10 11 mpbiran A ¬ A
13 9 12 sylibr ¬ y On y A A
14 sucdom2 n A suc n A
15 14 ad2antll n ω ¬ y On y A n A suc n A
16 nnon n ω n On
17 suceloni n On suc n On
18 breq1 y = suc n y A suc n A
19 18 rspcev suc n On suc n A y On y A
20 19 ex suc n On suc n A y On y A
21 16 17 20 3syl n ω suc n A y On y A
22 21 con3dimp n ω ¬ y On y A ¬ suc n A
23 22 adantrr n ω ¬ y 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 ω ¬ y On y A n A suc n A
26 25 exp32 n ω ¬ y On y A n A suc n A
27 2 3 4 13 26 finds2 x ω ¬ y On y A x A
28 27 com12 ¬ y On y A x ω x A
29 28 ralrimiv ¬ y On y A x ω x A
30 omsson ω On
31 ssrab ω x On | x A ω On x ω x A
32 30 31 mpbiran ω x On | x A x ω x A
33 29 32 sylibr ¬ y On y A ω x On | x A