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 nobdaymin ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ≠ ∅ ) → ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )
2 1 ancoms ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ) → ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )
3 2 3adant3 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )
4 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ No ) )
5 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑡 ∈ 𝐴 → 𝑡 ∈ No ) )
6 4 5 anim12d ⊢ ( 𝐴 ⊆ No → ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) ) )
7 6 imp ⊢ ( ( 𝐴 ⊆ No ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) )
8 7 ad2ant2r ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) )
9 nocvxminlem ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑤 <s 𝑡 ) )
10 9 imp ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ 𝑤 <s 𝑡 )
11 an2anr ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ↔ ( ( 𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) ) )
12 nocvxminlem ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑡 <s 𝑤 ) )
13 11 12 biimtrid ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑡 <s 𝑤 ) )
14 13 imp ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ 𝑡 <s 𝑤 )
15 slttrieq2 ⊢ ( ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) → ( 𝑤 = 𝑡 ↔ ( ¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤 ) ) )
16 15 biimpar ⊢ ( ( ( 𝑤 ∈ No ∧ 𝑡 ∈ No ) ∧ ( ¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤 ) ) → 𝑤 = 𝑡 )
17 8 10 14 16 syl12anc ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) ) ) → 𝑤 = 𝑡 )
18 17 exp32 ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) → ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) ) )
19 18 ralrimivv ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) )
20 19 3adant1 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) )
21 fveqeq2 ⊢ ( 𝑤 = 𝑡 → ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ↔ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) )
22 21 reu4 ⊢ ( ∃! 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ↔ ( ∃ 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐴 ( ( ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑡 ) = ∩ ( bday “ 𝐴 ) ) → 𝑤 = 𝑡 ) ) )
23 3 20 22 sylanbrc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ∃! 𝑤 ∈ 𝐴 ( bday ‘ 𝑤 ) = ∩ ( bday “ 𝐴 ) )