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