Metamath Proof Explorer

Theorem nobdaymin

Description: Any non-empty class of surreals has a birthday-minimal element. (Contributed by Scott Fenton, 11-Dec-2025)

Ref Expression
Assertion nobdaymin ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( bday ‘ 𝑥 ) = ∩ ( bday “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 imassrn ⊢ ( bday “ 𝐴 ) ⊆ ran bday
2 bdayrn ⊢ ran bday = On
3 1 2 sseqtri ⊢ ( bday “ 𝐴 ) ⊆ On
4 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5 bdaydm ⊢ dom bday = No
6 5 sseq2i ⊢ ( 𝐴 ⊆ dom bday ↔ 𝐴 ⊆ No )
7 bdayfun ⊢ Fun bday
8 funfvima2 ⊢ ( ( Fun bday ∧ 𝐴 ⊆ dom bday ) → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
9 7 8 mpan ⊢ ( 𝐴 ⊆ dom bday → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
10 6 9 sylbir ⊢ ( 𝐴 ⊆ No → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
11 ne0i ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) → ( bday “ 𝐴 ) ≠ ∅ )
12 10 11 syl6 ⊢ ( 𝐴 ⊆ No → ( 𝑥 ∈ 𝐴 → ( bday “ 𝐴 ) ≠ ∅ ) )
13 12 exlimdv ⊢ ( 𝐴 ⊆ No → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( bday “ 𝐴 ) ≠ ∅ ) )
14 4 13 biimtrid ⊢ ( 𝐴 ⊆ No → ( 𝐴 ≠ ∅ → ( bday “ 𝐴 ) ≠ ∅ ) )
15 14 imp ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ( bday “ 𝐴 ) ≠ ∅ )
16 onint ⊢ ( ( ( bday “ 𝐴 ) ⊆ On ∧ ( bday “ 𝐴 ) ≠ ∅ ) → ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) )
17 3 15 16 sylancr ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) )
18 bdayfn ⊢ bday Fn No
19 fvelimab ⊢ ( ( bday Fn No ∧ 𝐴 ⊆ No ) → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( bday ‘ 𝑥 ) = ∩ ( bday “ 𝐴 ) ) )
20 18 19 mpan ⊢ ( 𝐴 ⊆ No → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( bday ‘ 𝑥 ) = ∩ ( bday “ 𝐴 ) ) )
21 20 adantr ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( bday ‘ 𝑥 ) = ∩ ( bday “ 𝐴 ) ) )
22 17 21 mpbid ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( bday ‘ 𝑥 ) = ∩ ( bday “ 𝐴 ) )