Metamath Proof Explorer

Theorem nocvxminlem

Description: Lemma for nocvxmin . Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011)

Ref Expression
Assertion nocvxminlem ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑋 <s 𝑌 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 <s 𝑧 ↔ 𝑋 <s 𝑧 ) )
2 1 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) ↔ ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) ) )
3 2 imbi1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ↔ ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) )
4 3 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ↔ ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) )
5 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑧 <s 𝑦 ↔ 𝑧 <s 𝑌 ) )
6 5 anbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) ↔ ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) ) )
7 6 imbi1d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ↔ ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) ) )
8 7 ralbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ↔ ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) ) )
9 4 8 rspc2v ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) → ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) ) )
10 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑋 <s 𝑧 ↔ 𝑋 <s 𝑤 ) )
11 breq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 <s 𝑌 ↔ 𝑤 <s 𝑌 ) )
12 10 11 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) ↔ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
13 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
14 12 13 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) ↔ ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → 𝑤 ∈ 𝐴 ) ) )
15 14 rspcv ⊢ ( 𝑤 ∈ No → ( ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → 𝑤 ∈ 𝐴 ) ) )
16 bdaydm ⊢ dom bday = No
17 16 sseq2i ⊢ ( 𝐴 ⊆ dom bday ↔ 𝐴 ⊆ No )
18 bdayfun ⊢ Fun bday
19 funfvima2 ⊢ ( ( Fun bday ∧ 𝐴 ⊆ dom bday ) → ( 𝑤 ∈ 𝐴 → ( bday ‘ 𝑤 ) ∈ ( bday “ 𝐴 ) ) )
20 18 19 mpan ⊢ ( 𝐴 ⊆ dom bday → ( 𝑤 ∈ 𝐴 → ( bday ‘ 𝑤 ) ∈ ( bday “ 𝐴 ) ) )
21 17 20 sylbir ⊢ ( 𝐴 ⊆ No → ( 𝑤 ∈ 𝐴 → ( bday ‘ 𝑤 ) ∈ ( bday “ 𝐴 ) ) )
22 21 imp ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ( bday ‘ 𝑤 ) ∈ ( bday “ 𝐴 ) )
23 intss1 ⊢ ( ( bday ‘ 𝑤 ) ∈ ( bday “ 𝐴 ) → ∩ ( bday “ 𝐴 ) ⊆ ( bday ‘ 𝑤 ) )
24 22 23 syl ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ∩ ( bday “ 𝐴 ) ⊆ ( bday ‘ 𝑤 ) )
25 imassrn ⊢ ( bday “ 𝐴 ) ⊆ ran bday
26 bdayrn ⊢ ran bday = On
27 25 26 sseqtri ⊢ ( bday “ 𝐴 ) ⊆ On
28 22 ne0d ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ( bday “ 𝐴 ) ≠ ∅ )
29 oninton ⊢ ( ( ( bday “ 𝐴 ) ⊆ On ∧ ( bday “ 𝐴 ) ≠ ∅ ) → ∩ ( bday “ 𝐴 ) ∈ On )
30 27 28 29 sylancr ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ∩ ( bday “ 𝐴 ) ∈ On )
31 bdayelon ⊢ ( bday ‘ 𝑤 ) ∈ On
32 ontri1 ⊢ ( ( ∩ ( bday “ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑤 ) ∈ On ) → ( ∩ ( bday “ 𝐴 ) ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) ) )
33 30 31 32 sylancl ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ( ∩ ( bday “ 𝐴 ) ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) ) )
34 24 33 mpbid ⊢ ( ( 𝐴 ⊆ No ∧ 𝑤 ∈ 𝐴 ) → ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) )
35 34 ex ⊢ ( 𝐴 ⊆ No → ( 𝑤 ∈ 𝐴 → ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) ) )
36 eleq2 ⊢ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) → ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ↔ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) ) )
37 36 notbid ⊢ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) → ( ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) ) )
38 37 biimprcd ⊢ ( ¬ ( bday ‘ 𝑤 ) ∈ ∩ ( bday “ 𝐴 ) → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) )
39 35 38 syl6 ⊢ ( 𝐴 ⊆ No → ( 𝑤 ∈ 𝐴 → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) )
40 39 com3l ⊢ ( 𝑤 ∈ 𝐴 → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) → ( 𝐴 ⊆ No → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) )
41 40 adantrd ⊢ ( 𝑤 ∈ 𝐴 → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝐴 ⊆ No → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) )
42 15 41 syl8 ⊢ ( 𝑤 ∈ No → ( ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝐴 ⊆ No → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) )
43 42 com35 ⊢ ( 𝑤 ∈ No → ( ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) → ( 𝐴 ⊆ No → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) )
44 43 com4l ⊢ ( ∀ 𝑧 ∈ No ( ( 𝑋 <s 𝑧 ∧ 𝑧 <s 𝑌 ) → 𝑧 ∈ 𝐴 ) → ( 𝐴 ⊆ No → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝑤 ∈ No → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) )
45 9 44 syl6 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) → ( 𝐴 ⊆ No → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝑤 ∈ No → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) ) )
46 45 com3l ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) → ( 𝐴 ⊆ No → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝑤 ∈ No → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) ) )
47 46 impcom ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( 𝑤 ∈ No → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) ) ) ) )
48 47 imp42 ⊢ ( ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) ∧ 𝑤 ∈ No ) → ( ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) → ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) )
49 48 con2d ⊢ ( ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) ∧ 𝑤 ∈ No ) → ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → ¬ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
50 3anass ⊢ ( ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ↔ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
51 50 notbii ⊢ ( ¬ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ↔ ¬ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
52 imnan ⊢ ( ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → ¬ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) ↔ ¬ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
53 51 52 bitr4i ⊢ ( ¬ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ↔ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → ¬ ( 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) ) )
54 49 53 sylibr ⊢ ( ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) ∧ 𝑤 ∈ No ) → ¬ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) )
55 54 nrexdv ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ ∃ 𝑤 ∈ No ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) )
56 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑋 ∈ 𝐴 → 𝑋 ∈ No ) )
57 ssel ⊢ ( 𝐴 ⊆ No → ( 𝑌 ∈ 𝐴 → 𝑌 ∈ No ) )
58 56 57 anim12d ⊢ ( 𝐴 ⊆ No → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ) )
59 58 imp ⊢ ( ( 𝐴 ⊆ No ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) )
60 eqtr3 ⊢ ( ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) → ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) )
61 59 60 anim12i ⊢ ( ( ( 𝐴 ⊆ No ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) )
62 61 anasss ⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) )
63 62 adantlr ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) )
64 nodense ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ∧ 𝑋 <s 𝑌 ) ) → ∃ 𝑤 ∈ No ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) )
65 64 anassrs ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ∃ 𝑤 ∈ No ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) )
66 63 65 sylan ⊢ ( ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) ∧ 𝑋 <s 𝑌 ) → ∃ 𝑤 ∈ No ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ∧ 𝑋 <s 𝑤 ∧ 𝑤 <s 𝑌 ) )
67 55 66 mtand ⊢ ( ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) ∧ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) ) → ¬ 𝑋 <s 𝑌 )
68 67 ex ⊢ ( ( 𝐴 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ No ( ( 𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦 ) → 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ 𝐴 ) ∧ ( bday ‘ 𝑌 ) = ∩ ( bday “ 𝐴 ) ) ) → ¬ 𝑋 <s 𝑌 ) )