Metamath Proof Explorer

Theorem cardmin2

Description: The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion cardmin2 ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )

Proof

Step Hyp Ref Expression
1 onintrab2 ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On )
2 1 biimpi ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On )
3 2 adantr ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On )
4 eloni ⊢ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On → Ord ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
5 ordelss ⊢ ( ( Ord ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
6 4 5 sylan ⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
7 1 6 sylanb ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
8 ssdomg ⊢ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On → ( 𝑦 ⊆ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
9 3 7 8 sylc ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
10 onelon ⊢ ( ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ∈ On )
11 1 10 sylanb ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ∈ On )
12 nfcv ⊢ Ⅎ 𝑥 𝐴
13 nfcv ⊢ Ⅎ 𝑥 ≺
14 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
15 14 nfint ⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
16 12 13 15 nfbr ⊢ Ⅎ 𝑥 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 }
17 breq2 ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
18 16 17 onminsb ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
19 sdomentr ⊢ ( ( 𝐴 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → 𝐴 ≺ 𝑦 )
20 18 19 sylan ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → 𝐴 ≺ 𝑦 )
21 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ 𝑦 ) )
22 21 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) )
23 ssrab2 ⊢ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ On
24 onnmin ⊢ ( ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ⊆ On ∧ 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
25 23 24 mpan ⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
26 22 25 sylbir ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
27 26 expcom ⊢ ( 𝐴 ≺ 𝑦 → ( 𝑦 ∈ On → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
28 20 27 syl ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) → ( 𝑦 ∈ On → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
29 28 impancom ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ On ) → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
30 29 con2d ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) )
31 30 impancom ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ( 𝑦 ∈ On → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 ) )
32 11 31 mpd ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 )
33 ensym ⊢ ( 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≈ 𝑦 )
34 32 33 nsyl ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → ¬ 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
35 brsdom ⊢ ( 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( 𝑦 ≼ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∧ ¬ 𝑦 ≈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
36 9 34 35 sylanbrc ⊢ ( ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ∧ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) → 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
37 36 ralrimiva ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
38 iscard ⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ↔ ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ On ∧ ∀ 𝑦 ∈ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } 𝑦 ≺ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) )
39 2 37 38 sylanbrc ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 → ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
40 vprc ⊢ ¬ V ∈ V
41 inteq ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∩ ∅ )
42 int0 ⊢ ∩ ∅ = V
43 41 42 eqtrdi ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = V )
44 43 eleq1d ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ( ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ↔ V ∈ V ) )
45 40 44 mtbiri ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ¬ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V )
46 fvex ⊢ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ∈ V
47 eleq1 ⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) ∈ V ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V ) )
48 46 47 mpbii ⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ∈ V )
49 45 48 nsyl ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∅ → ¬ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
50 49 necon2ai ⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≠ ∅ )
51 rabn0 ⊢ ( { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )
52 50 51 sylib ⊢ ( ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } → ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 )
53 39 52 impbii ⊢ ( ∃ 𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ ( card ‘ ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )