Metamath Proof Explorer

Theorem nocvxmin

Description: Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of Alling p. 185. (Contributed by Scott Fenton, 30-Jun-2011)

Ref Expression
Assertion nocvxmin ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∃! 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 imassrn ⊢ ( bday “ 𝐴 ) ⊆ ran bday
2 bdayrn ⊢ ran bday = On
3 1 2 sseqtri ⊢ ( bday “ 𝐴 ) ⊆ On
4 bdaydm ⊢ dom bday = No
5 4 sseq2i ⊢ ( 𝐴 ⊆ dom bday ↔ 𝐴 ⊆ No )
6 bdayfun ⊢ Fun bday
7 funfvima2 ⊢ ( ( Fun bday ∧ 𝐴 ⊆ dom bday ) → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
8 6 7 mpan ⊢ ( 𝐴 ⊆ dom bday → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
9 5 8 sylbir ⊢ ( 𝐴 ⊆ No → ( 𝑥 ∈ 𝐴 → ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) ) )
10 elex2 ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ 𝐴 ) → ∃ 𝑤 𝑤 ∈ ( bday “ 𝐴 ) )
11 9 10 syl6 ⊢ ( 𝐴 ⊆ No → ( 𝑥 ∈ 𝐴 → ∃ 𝑤 𝑤 ∈ ( bday “ 𝐴 ) ) )
12 11 exlimdv ⊢ ( 𝐴 ⊆ No → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑤 𝑤 ∈ ( bday “ 𝐴 ) ) )
13 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
14 n0 ⊢ ( ( bday “ 𝐴 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( bday “ 𝐴 ) )
15 12 13 14 3imtr4g ⊢ ( 𝐴 ⊆ No → ( 𝐴 ≠ ∅ → ( bday “ 𝐴 ) ≠ ∅ ) )
16 15 impcom ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ) → ( bday “ 𝐴 ) ≠ ∅ )
17 onint ⊢ ( ( ( bday “ 𝐴 ) ⊆ On ∧ ( bday “ 𝐴 ) ≠ ∅ ) → ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) )
18 3 16 17 sylancr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ) → ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) )
19 bdayfn ⊢ bday Fn No
20 fvelimab ⊢ ( ( bday Fn No ∧ 𝐴 ⊆ No ) → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) )
21 19 20 mpan ⊢ ( 𝐴 ⊆ No → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) )
22 21 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ) → ( ∩ ( bday “ 𝐴 ) ∈ ( bday “ 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) )
23 18 22 mpbid ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ) → ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )
24 23 3adant3 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )
25 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ No ) )
26 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑡 ∈ 𝐴 → 𝑡 ∈ No ) )
27 25 26 anim12d ⊢ ( 𝐴 ⊆ No → ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) ) )
28 27 imp ⊢ ( ( 𝐴 ⊆ No ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) )
29 28 ad2ant2r ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) )
30 nocvxminlem ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑤 <s 𝑡 ) )
31 30 imp ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ 𝑤 <s 𝑡 )
32 ancom ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ↔ ( 𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) )
33 ancom ⊢ ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ↔ ( ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) )
34 32 33 anbi12i ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ↔ ( ( 𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) ) )
35 nocvxminlem ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑡 <s 𝑤 ) )
36 34 35 syl5bi ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑡 <s 𝑤 ) )
37 36 imp ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ 𝑡 <s 𝑤 )
38 slttrieq2 ⊢ ( ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) → ( 𝑤 = 𝑡 ↔ ( ¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤 ) ) )
39 38 biimpar ⊢ ( ( ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) ∧ ( ¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤 ) ) → 𝑤 = 𝑡 )
40 29 31 37 39 syl12anc ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → 𝑤 = 𝑡 )
41 40 exp32 ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) ) )
42 41 ralrimivv ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) )
43 42 3adant1 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) )
44 fveqeq2 ⊢ ( 𝑤 = 𝑡 → ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ↔ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) )
45 44 reu4 ⊢ ( ∃! 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ↔ ( ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) ) )
46 24 43 45 sylanbrc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∃! 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )