Metamath Proof Explorer

Theorem cofcutr

Description: If X is the cut of A and B , then A is cofinal with (LeftX ) and B is coinitial with ( RightX ) . Theorem 2.9 of Gonshor p. 12. (Contributed by Scott Fenton, 25-Sep-2024)

Ref Expression
Assertion cofcutr ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ) )

Proof

Step Hyp Ref Expression
1 bdayelon ⊢ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On
2 1 onssneli ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) → ¬ ( bday ‘ 𝑥 ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
3 leftssold ⊢ ( L ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
4 3 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( L ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
5 4 sselda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
6 bdayelon ⊢ ( bday ‘ 𝑋 ) ∈ On
7 leftssno ⊢ ( L ‘ 𝑋 ) ⊆ No
8 7 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( L ‘ 𝑋 ) ⊆ No )
9 8 sselda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝑥 ∈ No )
10 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝑋 ) ) )
11 6 9 10 sylancr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝑋 ) ) )
12 5 11 mpbid ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝑋 ) )
13 simplr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
14 13 fveq2d ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) = ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
15 12 14 eleqtrd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
16 2 15 nsyl3 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ¬ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) )
17 scutbday ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
18 17 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
19 bdayfn ⊢ bday Fn No
20 ssrab2 ⊢ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ⊆ No
21 sneq ⊢ ( 𝑡 = 𝑥 → { 𝑡 } = { 𝑥 } )
22 21 breq2d ⊢ ( 𝑡 = 𝑥 → ( 𝐴 <<s { 𝑡 } ↔ 𝐴 <<s { 𝑥 } ) )
23 21 breq1d ⊢ ( 𝑡 = 𝑥 → ( { 𝑡 } <<s 𝐵 ↔ { 𝑥 } <<s 𝐵 ) )
24 22 23 anbi12d ⊢ ( 𝑡 = 𝑥 → ( ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) )
25 9 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → 𝑥 ∈ No )
26 vsnex ⊢ { 𝑥 } ∈ V
27 26 a1i ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → { 𝑥 } ∈ V )
28 ssltex2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
29 28 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝐵 ∈ V )
30 9 snssd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → { 𝑥 } ⊆ No )
31 ssltss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
32 31 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝐵 ⊆ No )
33 9 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑥 ∈ No )
34 simpr ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
35 simpl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s 𝐵 )
36 35 scutcld ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( 𝐴 |s 𝐵 ) ∈ No )
37 34 36 eqeltrd ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝑋 ∈ No )
38 37 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑋 ∈ No )
39 32 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No )
40 leftval ⊢ ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 }
41 40 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } )
42 41 eleq2d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ) )
43 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) )
44 42 43 bitrdi ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ) )
45 44 simplbda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝑥 <s 𝑋 )
46 45 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑥 <s 𝑋 )
47 simpllr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
48 scutcut ⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
49 48 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
50 49 simp3d ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
51 ovex ⊢ ( 𝐴 |s 𝐵 ) ∈ V
52 51 snid ⊢ ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) }
53 ssltsepc ⊢ ( ( { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ∧ ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) } ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑏 )
54 52 53 mp3an2 ⊢ ( ( { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑏 )
55 50 54 sylan ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑏 )
56 47 55 eqbrtrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑋 <s 𝑏 )
57 33 38 39 46 56 slttrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑥 <s 𝑏 )
58 57 3adant2 ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑎 ∈ { 𝑥 } ∧ 𝑏 ∈ 𝐵 ) → 𝑥 <s 𝑏 )
59 velsn ⊢ ( 𝑎 ∈ { 𝑥 } ↔ 𝑎 = 𝑥 )
60 breq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏 ) )
61 59 60 sylbi ⊢ ( 𝑎 ∈ { 𝑥 } → ( 𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏 ) )
62 61 3ad2ant2 ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑎 ∈ { 𝑥 } ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏 ) )
63 58 62 mpbird ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑎 ∈ { 𝑥 } ∧ 𝑏 ∈ 𝐵 ) → 𝑎 <s 𝑏 )
64 27 29 30 32 63 ssltd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → { 𝑥 } <<s 𝐵 )
65 64 anim1ci ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) )
66 24 25 65 elrabd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → 𝑥 ∈ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } )
67 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ⊆ No ∧ 𝑥 ∈ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
68 19 20 66 67 mp3an12i ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
69 intss1 ⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
70 68 69 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
71 18 70 eqsstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝐴 <<s { 𝑥 } ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) )
72 16 71 mtand ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ¬ 𝐴 <<s { 𝑥 } )
73 ssltex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
74 73 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → 𝐴 ∈ V )
75 74 26 jctir ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → ( 𝐴 ∈ V ∧ { 𝑥 } ∈ V ) )
76 ssltss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
77 76 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → 𝐴 ⊆ No )
78 9 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → 𝑥 ∈ No )
79 78 snssd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → { 𝑥 } ⊆ No )
80 simpr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 )
81 77 79 80 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → ( 𝐴 ⊆ No ∧ { 𝑥 } ⊆ No ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) )
82 brsslt ⊢ ( 𝐴 <<s { 𝑥 } ↔ ( ( 𝐴 ∈ V ∧ { 𝑥 } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { 𝑥 } ⊆ No ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) ) )
83 75 81 82 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 ) → 𝐴 <<s { 𝑥 } )
84 72 83 mtand ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 )
85 rexnal ⊢ ( ∃ 𝑡 ∈ { 𝑥 } ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀ 𝑡 ∈ { 𝑥 } ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 )
86 ralcom ⊢ ( ∀ 𝑡 ∈ { 𝑥 } ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 )
87 85 86 xchbinx ⊢ ( ∃ 𝑡 ∈ { 𝑥 } ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ∀ 𝑡 ∈ { 𝑥 } 𝑦 <s 𝑡 )
88 84 87 sylibr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ∃ 𝑡 ∈ { 𝑥 } ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 )
89 vex ⊢ 𝑥 ∈ V
90 breq2 ⊢ ( 𝑡 = 𝑥 → ( 𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥 ) )
91 90 ralbidv ⊢ ( 𝑡 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ) )
92 91 notbid ⊢ ( 𝑡 = 𝑥 → ( ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ) )
93 89 92 rexsn ⊢ ( ∃ 𝑡 ∈ { 𝑥 } ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 )
94 88 93 sylib ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 )
95 76 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝐴 ⊆ No )
96 95 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ No )
97 slenlt ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( 𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥 ) )
98 9 96 97 syl2an2r ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥 ) )
99 98 rexbidva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥 ) )
100 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 )
101 99 100 bitrdi ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 <s 𝑥 ) )
102 94 101 mpbird ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ ( L ‘ 𝑋 ) ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 )
103 102 ralrimiva ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 )
104 1 onssneli ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) → ¬ ( bday ‘ 𝑧 ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
105 rightssold ⊢ ( R ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
106 105 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( R ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
107 106 sselda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
108 rightssno ⊢ ( R ‘ 𝑋 ) ⊆ No
109 108 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( R ‘ 𝑋 ) ⊆ No )
110 109 sselda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝑧 ∈ No )
111 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑧 ∈ No ) → ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑋 ) ) )
112 6 110 111 sylancr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑋 ) ) )
113 107 112 mpbid ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑋 ) )
114 simplr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
115 114 fveq2d ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) = ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
116 113 115 eleqtrd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑧 ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
117 104 116 nsyl3 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ¬ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) )
118 17 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
119 sneq ⊢ ( 𝑡 = 𝑧 → { 𝑡 } = { 𝑧 } )
120 119 breq2d ⊢ ( 𝑡 = 𝑧 → ( 𝐴 <<s { 𝑡 } ↔ 𝐴 <<s { 𝑧 } ) )
121 119 breq1d ⊢ ( 𝑡 = 𝑧 → ( { 𝑡 } <<s 𝐵 ↔ { 𝑧 } <<s 𝐵 ) )
122 120 121 anbi12d ⊢ ( 𝑡 = 𝑧 → ( ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑧 } ∧ { 𝑧 } <<s 𝐵 ) ) )
123 110 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → 𝑧 ∈ No )
124 73 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝐴 ∈ V )
125 vsnex ⊢ { 𝑧 } ∈ V
126 125 a1i ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → { 𝑧 } ∈ V )
127 76 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝐴 ⊆ No )
128 110 snssd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → { 𝑧 } ⊆ No )
129 127 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ No )
130 37 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑋 ∈ No )
131 110 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑧 ∈ No )
132 48 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
133 132 simp2d ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
134 ssltsepc ⊢ ( ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ 𝑎 ∈ 𝐴 ∧ ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) } ) → 𝑎 <s ( 𝐴 |s 𝐵 ) )
135 52 134 mp3an3 ⊢ ( ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s ( 𝐴 |s 𝐵 ) )
136 133 135 sylan ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s ( 𝐴 |s 𝐵 ) )
137 simpllr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
138 136 137 breqtrrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s 𝑋 )
139 rightval ⊢ ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 }
140 139 a1i ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } )
141 140 eleq2d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ) )
142 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) )
143 141 142 bitrdi ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) ) )
144 143 simplbda ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝑋 <s 𝑧 )
145 144 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑋 <s 𝑧 )
146 129 130 131 138 145 slttrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s 𝑧 )
147 146 3adant3 ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ { 𝑧 } ) → 𝑎 <s 𝑧 )
148 velsn ⊢ ( 𝑏 ∈ { 𝑧 } ↔ 𝑏 = 𝑧 )
149 breq2 ⊢ ( 𝑏 = 𝑧 → ( 𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧 ) )
150 148 149 sylbi ⊢ ( 𝑏 ∈ { 𝑧 } → ( 𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧 ) )
151 150 3ad2ant3 ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ { 𝑧 } ) → ( 𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧 ) )
152 147 151 mpbird ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ { 𝑧 } ) → 𝑎 <s 𝑏 )
153 124 126 127 128 152 ssltd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝐴 <<s { 𝑧 } )
154 153 anim1i ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → ( 𝐴 <<s { 𝑧 } ∧ { 𝑧 } <<s 𝐵 ) )
155 122 123 154 elrabd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → 𝑧 ∈ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } )
156 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ⊆ No ∧ 𝑧 ∈ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) → ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
157 19 20 155 156 mp3an12i ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
158 intss1 ⊢ ( ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑧 ) )
159 157 158 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑧 ) )
160 118 159 eqsstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ { 𝑧 } <<s 𝐵 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) )
161 117 160 mtand ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ¬ { 𝑧 } <<s 𝐵 )
162 28 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → 𝐵 ∈ V )
163 162 125 jctil ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → ( { 𝑧 } ∈ V ∧ 𝐵 ∈ V ) )
164 128 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → { 𝑧 } ⊆ No )
165 31 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → 𝐵 ⊆ No )
166 simpr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 )
167 164 165 166 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → ( { 𝑧 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) )
168 brsslt ⊢ ( { 𝑧 } <<s 𝐵 ↔ ( ( { 𝑧 } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { 𝑧 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) ) )
169 163 167 168 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ) → { 𝑧 } <<s 𝐵 )
170 161 169 mtand ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ¬ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 )
171 rexnal ⊢ ( ∃ 𝑡 ∈ { 𝑧 } ¬ ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀ 𝑡 ∈ { 𝑧 } ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 )
172 170 171 sylibr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ∃ 𝑡 ∈ { 𝑧 } ¬ ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 )
173 vex ⊢ 𝑧 ∈ V
174 breq1 ⊢ ( 𝑡 = 𝑧 → ( 𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤 ) )
175 174 ralbidv ⊢ ( 𝑡 = 𝑧 → ( ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 ) )
176 175 notbid ⊢ ( 𝑡 = 𝑧 → ( ¬ ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 ) )
177 173 176 rexsn ⊢ ( ∃ 𝑡 ∈ { 𝑧 } ¬ ∀ 𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 )
178 172 177 sylib ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ¬ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 )
179 31 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → 𝐵 ⊆ No )
180 179 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ No )
181 110 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝐵 ) → 𝑧 ∈ No )
182 slenlt ⊢ ( ( 𝑤 ∈ No ∧ 𝑧 ∈ No ) → ( 𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤 ) )
183 180 181 182 syl2anc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤 ) )
184 183 rexbidva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃ 𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤 ) )
185 rexnal ⊢ ( ∃ 𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤 ↔ ¬ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 )
186 184 185 bitrdi ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ( ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀ 𝑤 ∈ 𝐵 𝑧 <s 𝑤 ) )
187 178 186 mpbird ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ ( R ‘ 𝑋 ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 )
188 187 ralrimiva ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 )
189 103 188 jca ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ) )