Theorem cardmin

Description: The smallest ordinal that strictly dominates a set is a cardinal. (Contributed by NM, 28-Oct-2003) (Revised by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	cardmin	⊢ ( 𝐴 ∈ 𝑉 → ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		numthcor	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )
2		onintrab2	⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On )
3	1 2	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On )
4		onelon	⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ∈ On )
5	4	ex	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ∈ On ) )
6	3 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ∈ On ) )
7		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ 𝑦 ) )
8	7	onnminsb	⊢ ( 𝑦 ∈ On → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ 𝐴 ≺ 𝑦 ) )
9	6 8	syli	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ 𝐴 ≺ 𝑦 ) )
10		vex	⊢ 𝑦 ∈ V
11		domtri	⊢ ( ( 𝑦 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝑦 ) )
12	10 11	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝑦 ) )
13	9 12	sylibrd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ≼ 𝐴 ) )
14		nfcv	⊢ Ⅎ 𝑥 𝐴
15		nfcv	⊢ Ⅎ 𝑥 ≺
16		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
17	16	nfint	⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
18	14 15 17	nfbr	⊢ Ⅎ 𝑥 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
19		breq2	⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
20	18 19	onminsb	⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
21	1 20	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
22	13 21	jctird	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( 𝑦 ≼ 𝐴 ∧ 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ) )
23		domsdomtr	⊢ ( ( 𝑦 ≼ 𝐴 ∧ 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
24	22 23	syl6	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
25	24	ralrimiv	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
26		iscard	⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
27	3 25 26	sylanbrc	⊢ ( 𝐴 ∈ 𝑉 → ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )