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 ⊢ 𝐴 ∈ V
Assertion card2inf ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )

Proof

Step Hyp Ref Expression
1 card2inf.1 ⊢ 𝐴 ∈ V
2 breq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ≺ 𝐴 ↔ ∅ ≺ 𝐴 ) )
3 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ≺ 𝐴 ↔ 𝑛 ≺ 𝐴 ) )
4 breq1 ⊢ ( 𝑥 = suc 𝑛 → ( 𝑥 ≺ 𝐴 ↔ suc 𝑛 ≺ 𝐴 ) )
5 0elon ⊢ ∅ ∈ On
6 breq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ≈ 𝐴 ↔ ∅ ≈ 𝐴 ) )
7 6 rspcev ⊢ ( ( ∅ ∈ On ∧ ∅ ≈ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 )
8 5 7 mpan ⊢ ( ∅ ≈ 𝐴 → ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 )
9 8 con3i ⊢ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ¬ ∅ ≈ 𝐴 )
10 1 0dom ⊢ ∅ ≼ 𝐴
11 brsdom ⊢ ( ∅ ≺ 𝐴 ↔ ( ∅ ≼ 𝐴 ∧ ¬ ∅ ≈ 𝐴 ) )
12 10 11 mpbiran ⊢ ( ∅ ≺ 𝐴 ↔ ¬ ∅ ≈ 𝐴 )
13 9 12 sylibr ⊢ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ∅ ≺ 𝐴 )
14 sucdom2 ⊢ ( 𝑛 ≺ 𝐴 → suc 𝑛 ≼ 𝐴 )
15 14 ad2antll ⊢ ( ( 𝑛 ∈ ω ∧ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ∧ 𝑛 ≺ 𝐴 ) ) → suc 𝑛 ≼ 𝐴 )
16 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
17 suceloni ⊢ ( 𝑛 ∈ On → suc 𝑛 ∈ On )
18 breq1 ⊢ ( 𝑦 = suc 𝑛 → ( 𝑦 ≈ 𝐴 ↔ suc 𝑛 ≈ 𝐴 ) )
19 18 rspcev ⊢ ( ( suc 𝑛 ∈ On ∧ suc 𝑛 ≈ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 )
20 19 ex ⊢ ( suc 𝑛 ∈ On → ( suc 𝑛 ≈ 𝐴 → ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ) )
21 16 17 20 3syl ⊢ ( 𝑛 ∈ ω → ( suc 𝑛 ≈ 𝐴 → ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ) )
22 21 con3dimp ⊢ ( ( 𝑛 ∈ ω ∧ ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ) → ¬ suc 𝑛 ≈ 𝐴 )
23 22 adantrr ⊢ ( ( 𝑛 ∈ ω ∧ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ∧ 𝑛 ≺ 𝐴 ) ) → ¬ suc 𝑛 ≈ 𝐴 )
24 brsdom ⊢ ( suc 𝑛 ≺ 𝐴 ↔ ( suc 𝑛 ≼ 𝐴 ∧ ¬ suc 𝑛 ≈ 𝐴 ) )
25 15 23 24 sylanbrc ⊢ ( ( 𝑛 ∈ ω ∧ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 ∧ 𝑛 ≺ 𝐴 ) ) → suc 𝑛 ≺ 𝐴 )
26 25 exp32 ⊢ ( 𝑛 ∈ ω → ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ( 𝑛 ≺ 𝐴 → suc 𝑛 ≺ 𝐴 ) ) )
27 2 3 4 13 26 finds2 ⊢ ( 𝑥 ∈ ω → ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → 𝑥 ≺ 𝐴 ) )
28 27 com12 ⊢ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ( 𝑥 ∈ ω → 𝑥 ≺ 𝐴 ) )
29 28 ralrimiv ⊢ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ∀ 𝑥 ∈ ω 𝑥 ≺ 𝐴 )
30 omsson ⊢ ω ⊆ On
31 ssrab ⊢ ( ω ⊆ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ↔ ( ω ⊆ On ∧ ∀ 𝑥 ∈ ω 𝑥 ≺ 𝐴 ) )
32 30 31 mpbiran ⊢ ( ω ⊆ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } ↔ ∀ 𝑥 ∈ ω 𝑥 ≺ 𝐴 )
33 29 32 sylibr ⊢ ( ¬ ∃ 𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )