Metamath Proof Explorer

Theorem cutsun12

Description: Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Assertion cutsun12 ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( 𝐴 ∪ 𝐶 ) |s ( 𝐵 ∪ 𝐷 ) ) = ( 𝐴 |s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → 𝐴 <<s 𝐵 )
2 cutcuts ⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
3 1 2 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
4 3 simp2d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
5 simp2 ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } )
6 sltsun1 ⊢ ( ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ) → ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } )
7 4 5 6 syl2anc ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } )
8 3 simp3d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
9 simp3 ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 )
10 sltsun2 ⊢ ( ( { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) )
11 8 9 10 syl2anc ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) )
12 ovex ⊢ ( 𝐴 |s 𝐵 ) ∈ V
13 12 snnz ⊢ { ( 𝐴 |s 𝐵 ) } ≠ ∅
14 sltstr ⊢ ( ( ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ∧ { ( 𝐴 |s 𝐵 ) } ≠ ∅ ) → ( 𝐴 ∪ 𝐶 ) <<s ( 𝐵 ∪ 𝐷 ) )
15 13 14 mp3an3 ⊢ ( ( ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) <<s ( 𝐵 ∪ 𝐷 ) )
16 7 11 15 syl2anc ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝐴 ∪ 𝐶 ) <<s ( 𝐵 ∪ 𝐷 ) )
17 cutsval ⊢ ( ( 𝐴 ∪ 𝐶 ) <<s ( 𝐵 ∪ 𝐷 ) → ( ( 𝐴 ∪ 𝐶 ) |s ( 𝐵 ∪ 𝐷 ) ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) )
18 16 17 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( 𝐴 ∪ 𝐶 ) |s ( 𝐵 ∪ 𝐷 ) ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) )
19 vex ⊢ 𝑥 ∈ V
20 19 elima ⊢ ( 𝑥 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ∃ 𝑧 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } 𝑧 bday 𝑥 )
21 sneq ⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
22 21 breq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ↔ ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ) )
23 21 breq1d ⊢ ( 𝑦 = 𝑧 → ( { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ↔ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) )
24 22 23 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) ↔ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) )
25 24 rexrab ⊢ ( ∃ 𝑧 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } 𝑧 bday 𝑥 ↔ ∃ 𝑧 ∈ No ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ∧ 𝑧 bday 𝑥 ) )
26 20 25 bitri ⊢ ( 𝑥 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ∃ 𝑧 ∈ No ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ∧ 𝑧 bday 𝑥 ) )
27 simplr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → 𝑧 ∈ No )
28 bdayfn ⊢ bday Fn No
29 fnbrfvb ⊢ ( ( bday Fn No ∧ 𝑧 ∈ No ) → ( ( bday ‘ 𝑧 ) = 𝑥 ↔ 𝑧 bday 𝑥 ) )
30 28 29 mpan ⊢ ( 𝑧 ∈ No → ( ( bday ‘ 𝑧 ) = 𝑥 ↔ 𝑧 bday 𝑥 ) )
31 27 30 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( ( bday ‘ 𝑧 ) = 𝑥 ↔ 𝑧 bday 𝑥 ) )
32 simpll1 ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → 𝐴 <<s 𝐵 )
33 cutbday ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
34 32 33 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
35 simprl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } )
36 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐶 )
37 ssslts1 ⊢ ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐶 ) ) → 𝐴 <<s { 𝑧 } )
38 36 37 mpan2 ⊢ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } → 𝐴 <<s { 𝑧 } )
39 35 38 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → 𝐴 <<s { 𝑧 } )
40 simprr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) )
41 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ 𝐷 )
42 ssslts2 ⊢ ( ( { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ∧ 𝐵 ⊆ ( 𝐵 ∪ 𝐷 ) ) → { 𝑧 } <<s 𝐵 )
43 41 42 mpan2 ⊢ ( { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) → { 𝑧 } <<s 𝐵 )
44 40 43 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → { 𝑧 } <<s 𝐵 )
45 39 44 jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( 𝐴 <<s { 𝑧 } ∧ { 𝑧 } <<s 𝐵 ) )
46 21 breq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑧 } ) )
47 21 breq1d ⊢ ( 𝑦 = 𝑧 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑧 } <<s 𝐵 ) )
48 46 47 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑧 } ∧ { 𝑧 } <<s 𝐵 ) ) )
49 48 elrab ⊢ ( 𝑧 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑧 ∈ No ∧ ( 𝐴 <<s { 𝑧 } ∧ { 𝑧 } <<s 𝐵 ) ) )
50 27 45 49 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → 𝑧 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
51 ssrab2 ⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
52 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No ∧ 𝑧 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
53 28 51 52 mp3an12 ⊢ ( 𝑧 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } → ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
54 50 53 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
55 intss1 ⊢ ( ( bday ‘ 𝑧 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑧 ) )
56 54 55 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑧 ) )
57 34 56 eqsstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) )
58 sseq2 ⊢ ( ( bday ‘ 𝑧 ) = 𝑥 → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) ↔ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
59 58 biimpd ⊢ ( ( bday ‘ 𝑧 ) = 𝑥 → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
60 59 com12 ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑧 ) → ( ( bday ‘ 𝑧 ) = 𝑥 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
61 57 60 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( ( bday ‘ 𝑧 ) = 𝑥 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
62 31 61 sylbird ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ) → ( 𝑧 bday 𝑥 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
63 62 ex ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) → ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) → ( 𝑧 bday 𝑥 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) ) )
64 63 impd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ 𝑧 ∈ No ) → ( ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ∧ 𝑧 bday 𝑥 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
65 64 rexlimdva ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ∃ 𝑧 ∈ No ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( 𝐵 ∪ 𝐷 ) ) ∧ 𝑧 bday 𝑥 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
66 26 65 biimtrid ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝑥 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 ) )
67 66 ralrimiv ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ∀ 𝑥 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 )
68 ssint ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ∀ 𝑥 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑥 )
69 67 68 sylibr ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
70 3 simp1d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝐴 |s 𝐵 ) ∈ No )
71 7 11 jca ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ) )
72 sneq ⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → { 𝑦 } = { ( 𝐴 |s 𝐵 ) } )
73 72 breq2d ⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ↔ ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ) )
74 72 breq1d ⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ↔ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ) )
75 73 74 anbi12d ⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) ↔ ( ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ) ) )
76 75 elrab ⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( ( 𝐴 ∪ 𝐶 ) <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s ( 𝐵 ∪ 𝐷 ) ) ) )
77 70 71 76 sylanbrc ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } )
78 ssrab2 ⊢ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ⊆ No
79 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ⊆ No ∧ ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
80 28 78 79 mp3an12 ⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
81 77 80 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
82 intss1 ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ⊆ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
83 81 82 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ⊆ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
84 69 83 eqssd ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
85 conway ⊢ ( ( 𝐴 ∪ 𝐶 ) <<s ( 𝐵 ∪ 𝐷 ) → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
86 16 85 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) )
87 fveqeq2 ⊢ ( 𝑥 = ( 𝐴 |s 𝐵 ) → ( ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) )
88 87 riota2 ⊢ ( ( ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ∧ ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) = ( 𝐴 |s 𝐵 ) ) )
89 77 86 88 syl2anc ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ↔ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) = ( 𝐴 |s 𝐵 ) ) )
90 84 89 mpbid ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) = ( 𝐴 |s 𝐵 ) )
91 90 eqcomd ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( 𝐴 ∪ 𝐶 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ( 𝐵 ∪ 𝐷 ) ) } ) ) )
92 18 91 eqtr4d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → ( ( 𝐴 ∪ 𝐶 ) |s ( 𝐵 ∪ 𝐷 ) ) = ( 𝐴 |s 𝐵 ) )