Metamath Proof Explorer

Theorem eqscut2

Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion eqscut2 ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqscut ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ) ) )
2 eqss ⊢ ( ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ∧ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝑋 ) ) )
3 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
4 3 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐿 <<s { 𝑥 } ↔ 𝐿 <<s { 𝑋 } ) )
5 3 breq1d ⊢ ( 𝑥 = 𝑋 → ( { 𝑥 } <<s 𝑅 ↔ { 𝑋 } <<s 𝑅 ) )
6 4 5 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) )
7 6 elrab3 ⊢ ( 𝑋 ∈ No → ( 𝑋 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) )
8 7 adantl ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) )
9 8 biimpar ⊢ ( ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) ∧ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) → 𝑋 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } )
10 bdayfn ⊢ bday Fn No
11 ssrab2 ⊢ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ⊆ No
12 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ⊆ No ∧ 𝑋 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
13 10 11 12 mp3an12 ⊢ ( 𝑋 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
14 intss1 ⊢ ( ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝑋 ) )
15 9 13 14 3syl ⊢ ( ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) ∧ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝑋 ) )
16 15 biantrud ⊢ ( ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) ∧ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) → ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ∧ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝑋 ) ) ) )
17 ssint ⊢ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∀ 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ( bday ‘ 𝑋 ) ⊆ 𝑧 )
18 fvelimab ⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ⊆ No ) → ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ( bday ‘ 𝑦 ) = 𝑧 ) )
19 10 11 18 mp2an ⊢ ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ( bday ‘ 𝑦 ) = 𝑧 )
20 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
21 20 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐿 <<s { 𝑥 } ↔ 𝐿 <<s { 𝑦 } ) )
22 20 breq1d ⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } <<s 𝑅 ↔ { 𝑦 } <<s 𝑅 ) )
23 21 22 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ) )
24 23 rexrab ⊢ ( ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ( bday ‘ 𝑦 ) = 𝑧 ↔ ∃ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) )
25 19 24 bitri ⊢ ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∃ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) )
26 25 imbi1i ⊢ ( ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( ∃ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) )
27 r19.23v ⊢ ( ∀ 𝑦 ∈ No ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( ∃ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) )
28 eqcom ⊢ ( ( bday ‘ 𝑦 ) = 𝑧 ↔ 𝑧 = ( bday ‘ 𝑦 ) )
29 28 anbi1ci ⊢ ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) ↔ ( 𝑧 = ( bday ‘ 𝑦 ) ∧ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ) )
30 29 imbi1i ⊢ ( ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( ( 𝑧 = ( bday ‘ 𝑦 ) ∧ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) )
31 impexp ⊢ ( ( ( 𝑧 = ( bday ‘ 𝑦 ) ∧ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
32 30 31 bitri ⊢ ( ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
33 32 ralbii ⊢ ( ∀ 𝑦 ∈ No ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ∧ ( bday ‘ 𝑦 ) = 𝑧 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ∀ 𝑦 ∈ No ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
34 26 27 33 3bitr2i ⊢ ( ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ∀ 𝑦 ∈ No ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
35 34 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ No ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
36 df-ral ⊢ ( ∀ 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ( bday ‘ 𝑋 ) ⊆ 𝑧 ↔ ∀ 𝑧 ( 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) )
37 ralcom4 ⊢ ( ∀ 𝑦 ∈ No ∀ 𝑧 ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ No ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
38 35 36 37 3bitr4i ⊢ ( ∀ 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ( bday ‘ 𝑋 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ No ∀ 𝑧 ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) )
39 fvex ⊢ ( bday ‘ 𝑦 ) ∈ V
40 sseq2 ⊢ ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( bday ‘ 𝑋 ) ⊆ 𝑧 ↔ ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) )
41 40 imbi2d ⊢ ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ↔ ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) )
42 39 41 ceqsalv ⊢ ( ∀ 𝑧 ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) ↔ ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) )
43 42 ralbii ⊢ ( ∀ 𝑦 ∈ No ∀ 𝑧 ( 𝑧 = ( bday ‘ 𝑦 ) → ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) )
44 38 43 bitri ⊢ ( ∀ 𝑧 ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ( bday ‘ 𝑋 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) )
45 17 44 bitri ⊢ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) )
46 16 45 bitr3di ⊢ ( ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) ∧ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) → ( ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ∧ ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝑋 ) ) ↔ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) )
47 2 46 syl5bb ⊢ ( ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) ∧ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ) → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ↔ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) )
48 47 pm5.32da ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ) ↔ ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )
49 df-3an ⊢ ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ) ↔ ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ) )
50 df-3an ⊢ ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) ↔ ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ) ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) )
51 48 49 50 3bitr4g ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ) ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )
52 1 51 bitrd ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ∀ 𝑦 ∈ No ( ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )