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