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∈Ony≈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∈Ony≈A
8 5 7 mpan ⊢∅≈A→∃y∈Ony≈A
9 8 con3i ⊢¬∃y∈Ony≈A→¬∅≈A
10 1 0dom ⊢∅≼A
11 brsdom ⊢∅≺A↔∅≼A∧¬∅≈A
12 10 11 mpbiran ⊢∅≺A↔¬∅≈A
13 9 12 sylibr ⊢¬∃y∈Ony≈A→∅≺A
14 sucdom2 ⊢n≺A→suc⁡n≼A
15 14 ad2antll ⊢n∈ω∧¬∃y∈Ony≈A∧n≺A→suc⁡n≼A
16 nnon ⊢n∈ω→n∈On
17 onsuc ⊢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∈Ony≈A
20 19 ex ⊢suc⁡n∈On→suc⁡n≈A→∃y∈Ony≈A
21 16 17 20 3syl ⊢n∈ω→suc⁡n≈A→∃y∈Ony≈A
22 21 con3dimp ⊢n∈ω∧¬∃y∈Ony≈A→¬suc⁡n≈A
23 22 adantrr ⊢n∈ω∧¬∃y∈Ony≈A∧n≺A→¬suc⁡n≈A
24 brsdom ⊢suc⁡n≺A↔suc⁡n≼A∧¬suc⁡n≈A
25 15 23 24 sylanbrc ⊢n∈ω∧¬∃y∈Ony≈A∧n≺A→suc⁡n≺A
26 25 exp32 ⊢n∈ω→¬∃y∈Ony≈A→n≺A→suc⁡n≺A
27 2 3 4 13 26 finds2 ⊢x∈ω→¬∃y∈Ony≈A→x≺A
28 27 com12 ⊢¬∃y∈Ony≈A→x∈ω→x≺A
29 28 ralrimiv ⊢¬∃y∈Ony≈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∈Ony≈A→ω⊆x∈On|x≺A