Metamath Proof Explorer

Theorem madebdaylemlrcut

Description: Lemma for madebday . If the inductive hypothesis of madebday is satisfied up to the birthday of X , then the conclusion of lrcut holds. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebdaylemlrcut ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → L ⁡ X | s R ⁡ X = X

Proof

Step Hyp Ref Expression
1 ssltleft ⊢ X ∈ No → L ⁡ X ≪ s X
2 1 adantl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → L ⁡ X ≪ s X
3 ssltright ⊢ X ∈ No → X ≪ s R ⁡ X
4 3 adantl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → X ≪ s R ⁡ X
5 fveq2 ⊢ X = w → bday ⁡ X = bday ⁡ w
6 eqimss ⊢ bday ⁡ X = bday ⁡ w → bday ⁡ X ⊆ bday ⁡ w
7 5 6 syl ⊢ X = w → bday ⁡ X ⊆ bday ⁡ w
8 7 a1i ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → X = w → bday ⁡ X ⊆ bday ⁡ w
9 ssltsep ⊢ L ⁡ X ≪ s w → ∀ x ∈ L ⁡ X ∀ y ∈ w x < s y
10 vex ⊢ w ∈ V
11 breq2 ⊢ y = w → x < s y ↔ x < s w
12 10 11 ralsn ⊢ ∀ y ∈ w x < s y ↔ x < s w
13 12 ralbii ⊢ ∀ x ∈ L ⁡ X ∀ y ∈ w x < s y ↔ ∀ x ∈ L ⁡ X x < s w
14 9 13 sylib ⊢ L ⁡ X ≪ s w → ∀ x ∈ L ⁡ X x < s w
15 ssltsep ⊢ w ≪ s R ⁡ X → ∀ y ∈ w ∀ x ∈ R ⁡ X y < s x
16 breq1 ⊢ y = w → y < s x ↔ w < s x
17 16 ralbidv ⊢ y = w → ∀ x ∈ R ⁡ X y < s x ↔ ∀ x ∈ R ⁡ X w < s x
18 10 17 ralsn ⊢ ∀ y ∈ w ∀ x ∈ R ⁡ X y < s x ↔ ∀ x ∈ R ⁡ X w < s x
19 15 18 sylib ⊢ w ≪ s R ⁡ X → ∀ x ∈ R ⁡ X w < s x
20 14 19 anim12i ⊢ L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x
21 leftval ⊢ X ∈ No → L ⁡ X = z ∈ Old ⁡ bday ⁡ X | z < s X
22 21 raleqdv ⊢ X ∈ No → ∀ x ∈ L ⁡ X x < s w ↔ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | z < s X x < s w
23 rightval ⊢ X ∈ No → R ⁡ X = z ∈ Old ⁡ bday ⁡ X | X < s z
24 23 raleqdv ⊢ X ∈ No → ∀ x ∈ R ⁡ X w < s x ↔ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | X < s z w < s x
25 22 24 anbi12d ⊢ X ∈ No → ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x ↔ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | z < s X x < s w ∧ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | X < s z w < s x
26 breq1 ⊢ z = x → z < s X ↔ x < s X
27 26 ralrab ⊢ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | z < s X x < s w ↔ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w
28 breq2 ⊢ z = x → X < s z ↔ X < s x
29 28 ralrab ⊢ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | X < s z w < s x ↔ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x
30 27 29 anbi12i ⊢ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | z < s X x < s w ∧ ∀ x ∈ z ∈ Old ⁡ bday ⁡ X | X < s z w < s x ↔ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x
31 25 30 bitrdi ⊢ X ∈ No → ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x ↔ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x
32 31 ad2antlr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No → ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x ↔ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x
33 simplrl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → w ∈ No
34 sltirr ⊢ w ∈ No → ¬ w < s w
35 33 34 syl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → ¬ w < s w
36 bdayelon ⊢ bday ⁡ X ∈ On
37 bdayelon ⊢ bday ⁡ w ∈ On
38 ontri1 ⊢ bday ⁡ X ∈ On ∧ bday ⁡ w ∈ On → bday ⁡ X ⊆ bday ⁡ w ↔ ¬ bday ⁡ w ∈ bday ⁡ X
39 36 37 38 mp2an ⊢ bday ⁡ X ⊆ bday ⁡ w ↔ ¬ bday ⁡ w ∈ bday ⁡ X
40 39 con2bii ⊢ bday ⁡ w ∈ bday ⁡ X ↔ ¬ bday ⁡ X ⊆ bday ⁡ w
41 simplll ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
42 madebdaylemold ⊢ bday ⁡ X ∈ On ∧ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ w ∈ No → bday ⁡ w ∈ bday ⁡ X → w ∈ Old ⁡ bday ⁡ X
43 36 41 33 42 mp3an2i ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → bday ⁡ w ∈ bday ⁡ X → w ∈ Old ⁡ bday ⁡ X
44 slttrine ⊢ X ∈ No ∧ w ∈ No → X ≠ w ↔ X < s w ∨ w < s X
45 44 ad2ant2lr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X ≠ w ↔ X < s w ∨ w < s X
46 simprrr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x
47 breq2 ⊢ x = w → X < s x ↔ X < s w
48 breq2 ⊢ x = w → w < s x ↔ w < s w
49 47 48 imbi12d ⊢ x = w → X < s x → w < s x ↔ X < s w → w < s w
50 49 rspccv ⊢ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → w ∈ Old ⁡ bday ⁡ X → X < s w → w < s w
51 46 50 syl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → w ∈ Old ⁡ bday ⁡ X → X < s w → w < s w
52 51 com23 ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X < s w → w ∈ Old ⁡ bday ⁡ X → w < s w
53 simprrl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w
54 breq1 ⊢ x = w → x < s X ↔ w < s X
55 breq1 ⊢ x = w → x < s w ↔ w < s w
56 54 55 imbi12d ⊢ x = w → x < s X → x < s w ↔ w < s X → w < s w
57 56 rspccv ⊢ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w → w ∈ Old ⁡ bday ⁡ X → w < s X → w < s w
58 53 57 syl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → w ∈ Old ⁡ bday ⁡ X → w < s X → w < s w
59 58 com23 ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → w < s X → w ∈ Old ⁡ bday ⁡ X → w < s w
60 52 59 jaod ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X < s w ∨ w < s X → w ∈ Old ⁡ bday ⁡ X → w < s w
61 45 60 sylbid ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X ≠ w → w ∈ Old ⁡ bday ⁡ X → w < s w
62 61 imp ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → w ∈ Old ⁡ bday ⁡ X → w < s w
63 43 62 syld ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → bday ⁡ w ∈ bday ⁡ X → w < s w
64 40 63 syl5bir ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → ¬ bday ⁡ X ⊆ bday ⁡ w → w < s w
65 35 64 mt3d ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x ∧ X ≠ w → bday ⁡ X ⊆ bday ⁡ w
66 65 ex ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X ≠ w → bday ⁡ X ⊆ bday ⁡ w
67 66 expr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No → ∀ x ∈ Old ⁡ bday ⁡ X x < s X → x < s w ∧ ∀ x ∈ Old ⁡ bday ⁡ X X < s x → w < s x → X ≠ w → bday ⁡ X ⊆ bday ⁡ w
68 32 67 sylbid ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No → ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x → X ≠ w → bday ⁡ X ⊆ bday ⁡ w
69 68 impr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ ∀ x ∈ L ⁡ X x < s w ∧ ∀ x ∈ R ⁡ X w < s x → X ≠ w → bday ⁡ X ⊆ bday ⁡ w
70 20 69 sylanr2 ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → X ≠ w → bday ⁡ X ⊆ bday ⁡ w
71 8 70 pm2.61dne ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No ∧ L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → bday ⁡ X ⊆ bday ⁡ w
72 71 expr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No ∧ w ∈ No → L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → bday ⁡ X ⊆ bday ⁡ w
73 72 ralrimiva ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → ∀ w ∈ No L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → bday ⁡ X ⊆ bday ⁡ w
74 bdayfn ⊢ bday Fn No
75 ssrab2 ⊢ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ⊆ No
76 fnssintima ⊢ bday Fn No ∧ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ⊆ No → bday ⁡ X ⊆ ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ↔ ∀ w ∈ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X bday ⁡ X ⊆ bday ⁡ w
77 74 75 76 mp2an ⊢ bday ⁡ X ⊆ ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ↔ ∀ w ∈ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X bday ⁡ X ⊆ bday ⁡ w
78 sneq ⊢ z = w → z = w
79 78 breq2d ⊢ z = w → L ⁡ X ≪ s z ↔ L ⁡ X ≪ s w
80 78 breq1d ⊢ z = w → z ≪ s R ⁡ X ↔ w ≪ s R ⁡ X
81 79 80 anbi12d ⊢ z = w → L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ↔ L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X
82 81 ralrab ⊢ ∀ w ∈ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X bday ⁡ X ⊆ bday ⁡ w ↔ ∀ w ∈ No L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → bday ⁡ X ⊆ bday ⁡ w
83 77 82 bitri ⊢ bday ⁡ X ⊆ ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ↔ ∀ w ∈ No L ⁡ X ≪ s w ∧ w ≪ s R ⁡ X → bday ⁡ X ⊆ bday ⁡ w
84 73 83 sylibr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ⊆ ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
85 sneq ⊢ z = X → z = X
86 85 breq2d ⊢ z = X → L ⁡ X ≪ s z ↔ L ⁡ X ≪ s X
87 85 breq1d ⊢ z = X → z ≪ s R ⁡ X ↔ X ≪ s R ⁡ X
88 86 87 anbi12d ⊢ z = X → L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ↔ L ⁡ X ≪ s X ∧ X ≪ s R ⁡ X
89 simpr ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → X ∈ No
90 2 4 jca ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → L ⁡ X ≪ s X ∧ X ≪ s R ⁡ X
91 88 89 90 elrabd ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → X ∈ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
92 fnfvima ⊢ bday Fn No ∧ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ⊆ No ∧ X ∈ z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X → bday ⁡ X ∈ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
93 74 75 91 92 mp3an12i ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
94 intss1 ⊢ bday ⁡ X ∈ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X → ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ⊆ bday ⁡ X
95 93 94 syl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X ⊆ bday ⁡ X
96 84 95 eqssd ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X = ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
97 lltropt ⊢ X ∈ No → L ⁡ X ≪ s R ⁡ X
98 eqscut ⊢ L ⁡ X ≪ s R ⁡ X ∧ X ∈ No → L ⁡ X | s R ⁡ X = X ↔ L ⁡ X ≪ s X ∧ X ≪ s R ⁡ X ∧ bday ⁡ X = ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
99 97 98 mpancom ⊢ X ∈ No → L ⁡ X | s R ⁡ X = X ↔ L ⁡ X ≪ s X ∧ X ≪ s R ⁡ X ∧ bday ⁡ X = ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
100 99 adantl ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → L ⁡ X | s R ⁡ X = X ↔ L ⁡ X ≪ s X ∧ X ≪ s R ⁡ X ∧ bday ⁡ X = ⋂ bday z ∈ No | L ⁡ X ≪ s z ∧ z ≪ s R ⁡ X
101 2 4 96 100 mpbir3and ⊢ ∀ b ∈ bday ⁡ X ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → L ⁡ X | s R ⁡ X = X