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 ∣ 𝑥 ≺ 𝐴 } )