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 𝑌 ) )