Metamath Proof Explorer

Theorem nummin

Description: Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024)

Ref Expression
Assertion nummin ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ )

Proof

Step Hyp Ref Expression
1 cardf2 ⊢ card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On
2 ffun ⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → Fun card )
3 2 funfnd ⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → card Fn dom card )
4 1 3 ax-mp ⊢ card Fn dom card
5 fnimaeq0 ⊢ ( ( card Fn dom card ∧ 𝐴 ⊆ dom card ) → ( ( card “ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )
6 4 5 mpan ⊢ ( 𝐴 ⊆ dom card → ( ( card “ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )
7 6 necon3bid ⊢ ( 𝐴 ⊆ dom card → ( ( card “ 𝐴 ) ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
8 7 biimprd ⊢ ( 𝐴 ⊆ dom card → ( 𝐴 ≠ ∅ → ( card “ 𝐴 ) ≠ ∅ ) )
9 8 imdistani ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) )
10 fimass ⊢ ( card : { 𝑧 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑧 } ⟶ On → ( card “ 𝐴 ) ⊆ On )
11 1 10 ax-mp ⊢ ( card “ 𝐴 ) ⊆ On
12 onssmin ⊢ ( ( ( card “ 𝐴 ) ⊆ On ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 )
13 11 12 mpan ⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 )
14 ssel ⊢ ( ( card “ 𝐴 ) ⊆ On → ( 𝑧 ∈ ( card “ 𝐴 ) → 𝑧 ∈ On ) )
15 ssel ⊢ ( ( card “ 𝐴 ) ⊆ On → ( 𝑦 ∈ ( card “ 𝐴 ) → 𝑦 ∈ On ) )
16 14 15 anim12d ⊢ ( ( card “ 𝐴 ) ⊆ On → ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) ) )
17 11 16 ax-mp ⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) )
18 ontri1 ⊢ ( ( 𝑧 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧 ) )
19 17 18 syl ⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝑧 ) )
20 epel ⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
21 20 notbii ⊢ ( ¬ 𝑦 E 𝑧 ↔ ¬ 𝑦 ∈ 𝑧 )
22 19 21 bitr4di ⊢ ( ( 𝑧 ∈ ( card “ 𝐴 ) ∧ 𝑦 ∈ ( card “ 𝐴 ) ) → ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) )
23 22 rgen2 ⊢ ∀ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 )
24 r19.29r ⊢ ( ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) )
25 13 23 24 sylancl ⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) )
26 r19.26 ⊢ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) )
27 bicom1 ⊢ ( ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) → ( ¬ 𝑦 E 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
28 27 biimparc ⊢ ( ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ¬ 𝑦 E 𝑧 )
29 28 ralimi ⊢ ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ∧ ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 )
30 26 29 sylbir ⊢ ( ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 )
31 30 reximi ⊢ ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ( ∀ 𝑦 ∈ ( card “ 𝐴 ) 𝑧 ⊆ 𝑦 ∧ ∀ 𝑦 ∈ ( card “ 𝐴 ) ( 𝑧 ⊆ 𝑦 ↔ ¬ 𝑦 E 𝑧 ) ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 )
32 25 31 syl ⊢ ( ( card “ 𝐴 ) ≠ ∅ → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 )
33 32 adantl ⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 )
34 breq2 ⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( 𝑦 E 𝑧 ↔ 𝑦 E ( card ‘ 𝑥 ) ) )
35 34 notbid ⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( ¬ 𝑦 E 𝑧 ↔ ¬ 𝑦 E ( card ‘ 𝑥 ) ) )
36 35 ralbidv ⊢ ( 𝑧 = ( card ‘ 𝑥 ) → ( ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) )
37 36 rexima ⊢ ( ( card Fn dom card ∧ 𝐴 ⊆ dom card ) → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) )
38 4 37 mpan ⊢ ( 𝐴 ⊆ dom card → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) )
39 38 adantr ⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ( ∃ 𝑧 ∈ ( card “ 𝐴 ) ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) ) )
40 33 39 mpbid ⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) )
41 fvex ⊢ ( card ‘ 𝑥 ) ∈ V
42 41 dfpred3 ⊢ Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) }
43 42 eqeq1i ⊢ ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) } = ∅ )
44 rabeq0 ⊢ ( { 𝑦 ∈ ( card “ 𝐴 ) ∣ 𝑦 E ( card ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) )
45 43 44 bitri ⊢ ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) )
46 45 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ( card “ 𝐴 ) ¬ 𝑦 E ( card ‘ 𝑥 ) )
47 40 46 sylibr ⊢ ( ( 𝐴 ⊆ dom card ∧ ( card “ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ )
48 9 47 syl ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ )
49 ssel2 ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom card )
50 cardpred ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) )
51 50 eqeq1d ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ) )
52 predss ⊢ Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ 𝐴
53 sstr ⊢ ( ( Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom card ) → Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card )
54 52 53 mpan ⊢ ( 𝐴 ⊆ dom card → Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card )
55 fnimaeq0 ⊢ ( ( card Fn dom card ∧ Pred ( ≺ , 𝐴 , 𝑥 ) ⊆ dom card ) → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
56 4 54 55 sylancr ⊢ ( 𝐴 ⊆ dom card → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
57 56 adantr ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( ( card “ Pred ( ≺ , 𝐴 , 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
58 51 57 bitrd ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ dom card ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
59 49 58 syldan ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝑥 ∈ 𝐴 ) → ( Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
60 59 rexbidva ⊢ ( 𝐴 ⊆ dom card → ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
61 60 adantr ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 Pred ( E , ( card “ 𝐴 ) , ( card ‘ 𝑥 ) ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ ) )
62 48 61 mpbid ⊢ ( ( 𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 Pred ( ≺ , 𝐴 , 𝑥 ) = ∅ )