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 ( ≺ , 𝐴 , 𝑥 ) = ∅ )