Metamath Proof Explorer

Theorem addsuniflem

Description: Lemma for addsunif . State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsuniflem.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
addsuniflem.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
addsuniflem.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
addsuniflem.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion addsuniflem ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsuniflem.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2 addsuniflem.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3 addsuniflem.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4 addsuniflem.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5 1 cutscld ⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) ∈ No )
6 3 5 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ No )
7 2 cutscld ⊢ ( 𝜑 → ( 𝑀 |s 𝑆 ) ∈ No )
8 4 7 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ No )
9 addsval2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) )
10 6 8 9 syl2anc ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) )
11 6 8 addcuts ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) )
12 11 simp2d ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s { ( 𝐴 +s 𝐵 ) } )
13 11 simp3d ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) )
14 ovex ⊢ ( 𝐴 +s 𝐵 ) ∈ V
15 14 snnz ⊢ { ( 𝐴 +s 𝐵 ) } ≠ ∅
16 sltstr ⊢ ( ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ∧ { ( 𝐴 +s 𝐵 ) } ≠ ∅ ) → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) )
17 15 16 mp3an3 ⊢ ( ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s { ( 𝐴 +s 𝐵 ) } ∧ { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) )
18 12 13 17 syl2anc ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) <<s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) )
19 1 3 cofcutr1d ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 )
20 leftno ⊢ ( 𝑝 ∈ ( L ‘ 𝐴 ) → 𝑝 ∈ No )
21 20 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑙 ∈ 𝐿 ) → 𝑝 ∈ No )
22 sltsss1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
23 1 22 syl ⊢ ( 𝜑 → 𝐿 ⊆ No )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) → 𝐿 ⊆ No )
25 24 sselda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑙 ∈ 𝐿 ) → 𝑙 ∈ No )
26 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑙 ∈ 𝐿 ) → 𝐵 ∈ No )
27 21 25 26 leadds1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) ∧ 𝑙 ∈ 𝐿 ) → ( 𝑝 ≤s 𝑙 ↔ ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) ) )
28 27 rexbidva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( L ‘ 𝐴 ) ) → ( ∃ 𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) ) )
29 28 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑙 ∈ 𝐿 𝑝 ≤s 𝑙 ↔ ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) ) )
30 19 29 mpbid ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) )
31 eqeq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 = ( 𝑙 +s 𝐵 ) ↔ 𝑠 = ( 𝑙 +s 𝐵 ) ) )
32 31 rexbidv ⊢ ( 𝑦 = 𝑠 → ( ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) ↔ ∃ 𝑙 ∈ 𝐿 𝑠 = ( 𝑙 +s 𝐵 ) ) )
33 32 rexab ⊢ ( ∃ 𝑠 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ( 𝑝 +s 𝐵 ) ≤s 𝑠 ↔ ∃ 𝑠 ( ∃ 𝑙 ∈ 𝐿 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
34 rexcom4 ⊢ ( ∃ 𝑙 ∈ 𝐿 ∃ 𝑠 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ∃ 𝑠 ∃ 𝑙 ∈ 𝐿 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
35 ovex ⊢ ( 𝑙 +s 𝐵 ) ∈ V
36 breq2 ⊢ ( 𝑠 = ( 𝑙 +s 𝐵 ) → ( ( 𝑝 +s 𝐵 ) ≤s 𝑠 ↔ ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) ) )
37 35 36 ceqsexv ⊢ ( ∃ 𝑠 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) )
38 37 rexbii ⊢ ( ∃ 𝑙 ∈ 𝐿 ∃ 𝑠 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) )
39 r19.41v ⊢ ( ∃ 𝑙 ∈ 𝐿 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ( ∃ 𝑙 ∈ 𝐿 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
40 39 exbii ⊢ ( ∃ 𝑠 ∃ 𝑙 ∈ 𝐿 ( 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ∃ 𝑠 ( ∃ 𝑙 ∈ 𝐿 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
41 34 38 40 3bitr3ri ⊢ ( ∃ 𝑠 ( ∃ 𝑙 ∈ 𝐿 𝑠 = ( 𝑙 +s 𝐵 ) ∧ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) ↔ ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) )
42 33 41 bitri ⊢ ( ∃ 𝑠 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ( 𝑝 +s 𝐵 ) ≤s 𝑠 ↔ ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) )
43 ssun1 ⊢ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ⊆ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } )
44 ssrexv ⊢ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ⊆ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) → ( ∃ 𝑠 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ( 𝑝 +s 𝐵 ) ≤s 𝑠 → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
45 43 44 ax-mp ⊢ ( ∃ 𝑠 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ( 𝑝 +s 𝐵 ) ≤s 𝑠 → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
46 42 45 sylbir ⊢ ( ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
47 46 ralimi ⊢ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑙 ∈ 𝐿 ( 𝑝 +s 𝐵 ) ≤s ( 𝑙 +s 𝐵 ) → ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
48 30 47 syl ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
49 2 4 cofcutr1d ⊢ ( 𝜑 → ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 )
50 leftno ⊢ ( 𝑞 ∈ ( L ‘ 𝐵 ) → 𝑞 ∈ No )
51 50 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝑞 ∈ No )
52 sltsss1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ⊆ No )
53 2 52 syl ⊢ ( 𝜑 → 𝑀 ⊆ No )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) → 𝑀 ⊆ No )
55 54 sselda ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝑚 ∈ No )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝐴 ∈ No )
57 51 55 56 leadds2d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ 𝑚 ∈ 𝑀 ) → ( 𝑞 ≤s 𝑚 ↔ ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) ) )
58 57 rexbidva ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) → ( ∃ 𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) ) )
59 58 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑚 ∈ 𝑀 𝑞 ≤s 𝑚 ↔ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) ) )
60 49 59 mpbid ⊢ ( 𝜑 → ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) )
61 eqeq1 ⊢ ( 𝑧 = 𝑠 → ( 𝑧 = ( 𝐴 +s 𝑚 ) ↔ 𝑠 = ( 𝐴 +s 𝑚 ) ) )
62 61 rexbidv ⊢ ( 𝑧 = 𝑠 → ( ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) ↔ ∃ 𝑚 ∈ 𝑀 𝑠 = ( 𝐴 +s 𝑚 ) ) )
63 62 rexab ⊢ ( ∃ 𝑠 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ( 𝐴 +s 𝑞 ) ≤s 𝑠 ↔ ∃ 𝑠 ( ∃ 𝑚 ∈ 𝑀 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
64 rexcom4 ⊢ ( ∃ 𝑚 ∈ 𝑀 ∃ 𝑠 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ∃ 𝑠 ∃ 𝑚 ∈ 𝑀 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
65 ovex ⊢ ( 𝐴 +s 𝑚 ) ∈ V
66 breq2 ⊢ ( 𝑠 = ( 𝐴 +s 𝑚 ) → ( ( 𝐴 +s 𝑞 ) ≤s 𝑠 ↔ ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) ) )
67 65 66 ceqsexv ⊢ ( ∃ 𝑠 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) )
68 67 rexbii ⊢ ( ∃ 𝑚 ∈ 𝑀 ∃ 𝑠 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) )
69 r19.41v ⊢ ( ∃ 𝑚 ∈ 𝑀 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ( ∃ 𝑚 ∈ 𝑀 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
70 69 exbii ⊢ ( ∃ 𝑠 ∃ 𝑚 ∈ 𝑀 ( 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ∃ 𝑠 ( ∃ 𝑚 ∈ 𝑀 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
71 64 68 70 3bitr3ri ⊢ ( ∃ 𝑠 ( ∃ 𝑚 ∈ 𝑀 𝑠 = ( 𝐴 +s 𝑚 ) ∧ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) ↔ ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) )
72 63 71 bitri ⊢ ( ∃ 𝑠 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ( 𝐴 +s 𝑞 ) ≤s 𝑠 ↔ ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) )
73 ssun2 ⊢ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ⊆ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } )
74 ssrexv ⊢ ( { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ⊆ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) → ( ∃ 𝑠 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ( 𝐴 +s 𝑞 ) ≤s 𝑠 → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
75 73 74 ax-mp ⊢ ( ∃ 𝑠 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ( 𝐴 +s 𝑞 ) ≤s 𝑠 → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
76 72 75 sylbir ⊢ ( ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
77 76 ralimi ⊢ ( ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑚 ∈ 𝑀 ( 𝐴 +s 𝑞 ) ≤s ( 𝐴 +s 𝑚 ) → ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
78 60 77 syl ⊢ ( 𝜑 → ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
79 ralunb ⊢ ( ∀ 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ( ∀ 𝑟 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ∧ ∀ 𝑟 ∈ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
80 eqeq1 ⊢ ( 𝑎 = 𝑟 → ( 𝑎 = ( 𝑝 +s 𝐵 ) ↔ 𝑟 = ( 𝑝 +s 𝐵 ) ) )
81 80 rexbidv ⊢ ( 𝑎 = 𝑟 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑟 = ( 𝑝 +s 𝐵 ) ) )
82 81 ralab ⊢ ( ∀ 𝑟 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∀ 𝑟 ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
83 ralcom4 ⊢ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∀ 𝑟 ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑟 ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
84 ovex ⊢ ( 𝑝 +s 𝐵 ) ∈ V
85 breq1 ⊢ ( 𝑟 = ( 𝑝 +s 𝐵 ) → ( 𝑟 ≤s 𝑠 ↔ ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
86 85 rexbidv ⊢ ( 𝑟 = ( 𝑝 +s 𝐵 ) → ( ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 ) )
87 84 86 ceqsalv ⊢ ( ∀ 𝑟 ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
88 87 ralbii ⊢ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∀ 𝑟 ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
89 r19.23v ⊢ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
90 89 albii ⊢ ( ∀ 𝑟 ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ( 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑟 ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
91 83 88 90 3bitr3ri ⊢ ( ∀ 𝑟 ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑟 = ( 𝑝 +s 𝐵 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
92 82 91 bitri ⊢ ( ∀ 𝑟 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 )
93 eqeq1 ⊢ ( 𝑏 = 𝑟 → ( 𝑏 = ( 𝐴 +s 𝑞 ) ↔ 𝑟 = ( 𝐴 +s 𝑞 ) ) )
94 93 rexbidv ⊢ ( 𝑏 = 𝑟 → ( ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) ↔ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑟 = ( 𝐴 +s 𝑞 ) ) )
95 94 ralab ⊢ ( ∀ 𝑟 ∈ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∀ 𝑟 ( ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
96 ralcom4 ⊢ ( ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∀ 𝑟 ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑟 ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
97 ovex ⊢ ( 𝐴 +s 𝑞 ) ∈ V
98 breq1 ⊢ ( 𝑟 = ( 𝐴 +s 𝑞 ) → ( 𝑟 ≤s 𝑠 ↔ ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
99 98 rexbidv ⊢ ( 𝑟 = ( 𝐴 +s 𝑞 ) → ( ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
100 97 99 ceqsalv ⊢ ( ∀ 𝑟 ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
101 100 ralbii ⊢ ( ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∀ 𝑟 ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
102 r19.23v ⊢ ( ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ( ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
103 102 albii ⊢ ( ∀ 𝑟 ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ( 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑟 ( ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) )
104 96 101 103 3bitr3ri ⊢ ( ∀ 𝑟 ( ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑟 = ( 𝐴 +s 𝑞 ) → ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
105 95 104 bitri ⊢ ( ∀ 𝑟 ∈ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 )
106 92 105 anbi12i ⊢ ( ( ∀ 𝑟 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ∧ ∀ 𝑟 ∈ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ) ↔ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 ∧ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
107 79 106 bitri ⊢ ( ∀ 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 ↔ ( ∀ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝑝 +s 𝐵 ) ≤s 𝑠 ∧ ∀ 𝑞 ∈ ( L ‘ 𝐵 ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ( 𝐴 +s 𝑞 ) ≤s 𝑠 ) )
108 48 78 107 sylanbrc ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) ∃ 𝑠 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) 𝑟 ≤s 𝑠 )
109 1 3 cofcutr2d ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 )
110 sltsss2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
111 1 110 syl ⊢ ( 𝜑 → 𝑅 ⊆ No )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) → 𝑅 ⊆ No )
113 112 sselda ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ No )
114 rightno ⊢ ( 𝑒 ∈ ( R ‘ 𝐴 ) → 𝑒 ∈ No )
115 114 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑒 ∈ No )
116 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝐵 ∈ No )
117 113 115 116 leadds1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 ≤s 𝑒 ↔ ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) ) )
118 117 rexbidva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( R ‘ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) ) )
119 118 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑟 ∈ 𝑅 𝑟 ≤s 𝑒 ↔ ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) ) )
120 109 119 mpbid ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) )
121 eqeq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 = ( 𝑟 +s 𝐵 ) ↔ 𝑏 = ( 𝑟 +s 𝐵 ) ) )
122 121 rexbidv ⊢ ( 𝑤 = 𝑏 → ( ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) ↔ ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ) )
123 122 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } 𝑏 ≤s ( 𝑒 +s 𝐵 ) ↔ ∃ 𝑏 ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
124 rexcom4 ⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑏 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ∃ 𝑏 ∃ 𝑟 ∈ 𝑅 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
125 ovex ⊢ ( 𝑟 +s 𝐵 ) ∈ V
126 breq1 ⊢ ( 𝑏 = ( 𝑟 +s 𝐵 ) → ( 𝑏 ≤s ( 𝑒 +s 𝐵 ) ↔ ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) ) )
127 125 126 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) )
128 127 rexbii ⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑏 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) )
129 r19.41v ⊢ ( ∃ 𝑟 ∈ 𝑅 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
130 129 exbii ⊢ ( ∃ 𝑏 ∃ 𝑟 ∈ 𝑅 ( 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ∃ 𝑏 ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
131 124 128 130 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∧ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) )
132 123 131 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } 𝑏 ≤s ( 𝑒 +s 𝐵 ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) )
133 ssun1 ⊢ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ⊆ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } )
134 ssrexv ⊢ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ⊆ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → ( ∃ 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } 𝑏 ≤s ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
135 133 134 ax-mp ⊢ ( ∃ 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } 𝑏 ≤s ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
136 132 135 sylbir ⊢ ( ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
137 136 ralimi ⊢ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑟 ∈ 𝑅 ( 𝑟 +s 𝐵 ) ≤s ( 𝑒 +s 𝐵 ) → ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
138 120 137 syl ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
139 2 4 cofcutr2d ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 )
140 sltsss2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ⊆ No )
141 2 140 syl ⊢ ( 𝜑 → 𝑆 ⊆ No )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) → 𝑆 ⊆ No )
143 142 sselda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ No )
144 rightno ⊢ ( 𝑓 ∈ ( R ‘ 𝐵 ) → 𝑓 ∈ No )
145 144 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → 𝑓 ∈ No )
146 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → 𝐴 ∈ No )
147 143 145 146 leadds2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑠 ≤s 𝑓 ↔ ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) ) )
148 147 rexbidva ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( R ‘ 𝐵 ) ) → ( ∃ 𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) ) )
149 148 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑠 ∈ 𝑆 𝑠 ≤s 𝑓 ↔ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) ) )
150 139 149 mpbid ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) )
151 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝐴 +s 𝑠 ) ↔ 𝑏 = ( 𝐴 +s 𝑠 ) ) )
152 151 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) ↔ ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ) )
153 152 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } 𝑏 ≤s ( 𝐴 +s 𝑓 ) ↔ ∃ 𝑏 ( ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
154 rexcom4 ⊢ ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑏 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ∃ 𝑏 ∃ 𝑠 ∈ 𝑆 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
155 ovex ⊢ ( 𝐴 +s 𝑠 ) ∈ V
156 breq1 ⊢ ( 𝑏 = ( 𝐴 +s 𝑠 ) → ( 𝑏 ≤s ( 𝐴 +s 𝑓 ) ↔ ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) ) )
157 155 156 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) )
158 157 rexbii ⊢ ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑏 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) )
159 r19.41v ⊢ ( ∃ 𝑠 ∈ 𝑆 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ( ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
160 159 exbii ⊢ ( ∃ 𝑏 ∃ 𝑠 ∈ 𝑆 ( 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ∃ 𝑏 ( ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
161 154 158 160 3bitr3ri ⊢ ( ∃ 𝑏 ( ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ∧ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) )
162 153 161 bitri ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } 𝑏 ≤s ( 𝐴 +s 𝑓 ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) )
163 ssun2 ⊢ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ⊆ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } )
164 ssrexv ⊢ ( { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ⊆ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } 𝑏 ≤s ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
165 163 164 ax-mp ⊢ ( ∃ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } 𝑏 ≤s ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
166 162 165 sylbir ⊢ ( ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
167 166 ralimi ⊢ ( ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑠 ∈ 𝑆 ( 𝐴 +s 𝑠 ) ≤s ( 𝐴 +s 𝑓 ) → ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
168 150 167 syl ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
169 ralunb ⊢ ( ∀ 𝑎 ∈ ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ( ∀ 𝑎 ∈ { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ∧ ∀ 𝑎 ∈ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
170 eqeq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 = ( 𝑒 +s 𝐵 ) ↔ 𝑎 = ( 𝑒 +s 𝐵 ) ) )
171 170 rexbidv ⊢ ( 𝑐 = 𝑎 → ( ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) ↔ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑒 +s 𝐵 ) ) )
172 171 ralab ⊢ ( ∀ 𝑎 ∈ { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑎 ( ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
173 ralcom4 ⊢ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∀ 𝑎 ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑎 ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
174 ovex ⊢ ( 𝑒 +s 𝐵 ) ∈ V
175 breq2 ⊢ ( 𝑎 = ( 𝑒 +s 𝐵 ) → ( 𝑏 ≤s 𝑎 ↔ 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
176 175 rexbidv ⊢ ( 𝑎 = ( 𝑒 +s 𝐵 ) → ( ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) ) )
177 174 176 ceqsalv ⊢ ( ∀ 𝑎 ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
178 177 ralbii ⊢ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∀ 𝑎 ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
179 r19.23v ⊢ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ( ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
180 179 albii ⊢ ( ∀ 𝑎 ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ( 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑎 ( ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
181 173 178 180 3bitr3ri ⊢ ( ∀ 𝑎 ( ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑒 +s 𝐵 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
182 172 181 bitri ⊢ ( ∀ 𝑎 ∈ { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) )
183 eqeq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 = ( 𝐴 +s 𝑓 ) ↔ 𝑎 = ( 𝐴 +s 𝑓 ) ) )
184 183 rexbidv ⊢ ( 𝑑 = 𝑎 → ( ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) ↔ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑎 = ( 𝐴 +s 𝑓 ) ) )
185 184 ralab ⊢ ( ∀ 𝑎 ∈ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑎 ( ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
186 ralcom4 ⊢ ( ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∀ 𝑎 ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑎 ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
187 ovex ⊢ ( 𝐴 +s 𝑓 ) ∈ V
188 breq2 ⊢ ( 𝑎 = ( 𝐴 +s 𝑓 ) → ( 𝑏 ≤s 𝑎 ↔ 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
189 188 rexbidv ⊢ ( 𝑎 = ( 𝐴 +s 𝑓 ) → ( ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
190 187 189 ceqsalv ⊢ ( ∀ 𝑎 ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
191 190 ralbii ⊢ ( ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∀ 𝑎 ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
192 r19.23v ⊢ ( ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ( ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
193 192 albii ⊢ ( ∀ 𝑎 ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ( 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑎 ( ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) )
194 186 191 193 3bitr3ri ⊢ ( ∀ 𝑎 ( ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑎 = ( 𝐴 +s 𝑓 ) → ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
195 185 194 bitri ⊢ ( ∀ 𝑎 ∈ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) )
196 182 195 anbi12i ⊢ ( ( ∀ 𝑎 ∈ { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ∧ ∀ 𝑎 ∈ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ) ↔ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) ∧ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
197 169 196 bitri ⊢ ( ∀ 𝑎 ∈ ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 ↔ ( ∀ 𝑒 ∈ ( R ‘ 𝐴 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝑒 +s 𝐵 ) ∧ ∀ 𝑓 ∈ ( R ‘ 𝐵 ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s ( 𝐴 +s 𝑓 ) ) )
198 138 168 197 sylanbrc ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ∃ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) 𝑏 ≤s 𝑎 )
199 eqid ⊢ ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) = ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) )
200 199 rnmpt ⊢ ran ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) = { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) }
201 sltsex1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
202 1 201 syl ⊢ ( 𝜑 → 𝐿 ∈ V )
203 202 mptexd ⊢ ( 𝜑 → ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) ∈ V )
204 rnexg ⊢ ( ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) ∈ V → ran ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) ∈ V )
205 203 204 syl ⊢ ( 𝜑 → ran ( 𝑙 ∈ 𝐿 ↦ ( 𝑙 +s 𝐵 ) ) ∈ V )
206 200 205 eqeltrrid ⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∈ V )
207 eqid ⊢ ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) = ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) )
208 207 rnmpt ⊢ ran ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) = { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) }
209 sltsex1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ∈ V )
210 2 209 syl ⊢ ( 𝜑 → 𝑀 ∈ V )
211 210 mptexd ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) ∈ V )
212 rnexg ⊢ ( ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) ∈ V → ran ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) ∈ V )
213 211 212 syl ⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝑀 ↦ ( 𝐴 +s 𝑚 ) ) ∈ V )
214 208 213 eqeltrrid ⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ∈ V )
215 206 214 unexd ⊢ ( 𝜑 → ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ∈ V )
216 snex ⊢ { ( 𝐴 +s 𝐵 ) } ∈ V
217 216 a1i ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } ∈ V )
218 23 sselda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝑙 ∈ No )
219 8 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝐵 ∈ No )
220 218 219 addscld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝑙 +s 𝐵 ) ∈ No )
221 eleq1 ⊢ ( 𝑦 = ( 𝑙 +s 𝐵 ) → ( 𝑦 ∈ No ↔ ( 𝑙 +s 𝐵 ) ∈ No ) )
222 220 221 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝑦 = ( 𝑙 +s 𝐵 ) → 𝑦 ∈ No ) )
223 222 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) → 𝑦 ∈ No ) )
224 223 abssdv ⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ⊆ No )
225 6 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝐴 ∈ No )
226 53 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝑚 ∈ No )
227 225 226 addscld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝐴 +s 𝑚 ) ∈ No )
228 eleq1 ⊢ ( 𝑧 = ( 𝐴 +s 𝑚 ) → ( 𝑧 ∈ No ↔ ( 𝐴 +s 𝑚 ) ∈ No ) )
229 227 228 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑧 = ( 𝐴 +s 𝑚 ) → 𝑧 ∈ No ) )
230 229 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) → 𝑧 ∈ No ) )
231 230 abssdv ⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ⊆ No )
232 224 231 unssd ⊢ ( 𝜑 → ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ⊆ No )
233 6 8 addscld ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
234 233 snssd ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } ⊆ No )
235 velsn ⊢ ( 𝑏 ∈ { ( 𝐴 +s 𝐵 ) } ↔ 𝑏 = ( 𝐴 +s 𝐵 ) )
236 elun ⊢ ( 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ↔ ( 𝑎 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∨ 𝑎 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) )
237 vex ⊢ 𝑎 ∈ V
238 eqeq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 = ( 𝑙 +s 𝐵 ) ↔ 𝑎 = ( 𝑙 +s 𝐵 ) ) )
239 238 rexbidv ⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) ↔ ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) ) )
240 237 239 elab ⊢ ( 𝑎 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ↔ ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) )
241 eqeq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 = ( 𝐴 +s 𝑚 ) ↔ 𝑎 = ( 𝐴 +s 𝑚 ) ) )
242 241 rexbidv ⊢ ( 𝑧 = 𝑎 → ( ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) ↔ ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) ) )
243 237 242 elab ⊢ ( 𝑎 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ↔ ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) )
244 240 243 orbi12i ⊢ ( ( 𝑎 ∈ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∨ 𝑎 ∈ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) ∨ ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) ) )
245 236 244 bitri ⊢ ( 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) ∨ ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) ) )
246 cutcuts ⊢ ( 𝐿 <<s 𝑅 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
247 1 246 syl ⊢ ( 𝜑 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
248 247 simp2d ⊢ ( 𝜑 → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
249 248 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
250 simpr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝑙 ∈ 𝐿 )
251 ovex ⊢ ( 𝐿 |s 𝑅 ) ∈ V
252 251 snid ⊢ ( 𝐿 |s 𝑅 ) ∈ { ( 𝐿 |s 𝑅 ) }
253 252 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝐿 |s 𝑅 ) ∈ { ( 𝐿 |s 𝑅 ) } )
254 249 250 253 sltssepcd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝑙 <s ( 𝐿 |s 𝑅 ) )
255 3 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝐴 = ( 𝐿 |s 𝑅 ) )
256 254 255 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝑙 <s 𝐴 )
257 6 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → 𝐴 ∈ No )
258 218 257 219 ltadds1d ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝑙 <s 𝐴 ↔ ( 𝑙 +s 𝐵 ) <s ( 𝐴 +s 𝐵 ) ) )
259 256 258 mpbid ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝑙 +s 𝐵 ) <s ( 𝐴 +s 𝐵 ) )
260 breq1 ⊢ ( 𝑎 = ( 𝑙 +s 𝐵 ) → ( 𝑎 <s ( 𝐴 +s 𝐵 ) ↔ ( 𝑙 +s 𝐵 ) <s ( 𝐴 +s 𝐵 ) ) )
261 259 260 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐿 ) → ( 𝑎 = ( 𝑙 +s 𝐵 ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
262 261 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
263 cutcuts ⊢ ( 𝑀 <<s 𝑆 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
264 2 263 syl ⊢ ( 𝜑 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
265 264 simp2d ⊢ ( 𝜑 → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
266 265 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
267 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝑚 ∈ 𝑀 )
268 ovex ⊢ ( 𝑀 |s 𝑆 ) ∈ V
269 268 snid ⊢ ( 𝑀 |s 𝑆 ) ∈ { ( 𝑀 |s 𝑆 ) }
270 269 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑀 |s 𝑆 ) ∈ { ( 𝑀 |s 𝑆 ) } )
271 266 267 270 sltssepcd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝑚 <s ( 𝑀 |s 𝑆 ) )
272 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝐵 = ( 𝑀 |s 𝑆 ) )
273 271 272 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝑚 <s 𝐵 )
274 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → 𝐵 ∈ No )
275 226 274 225 ltadds2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑚 <s 𝐵 ↔ ( 𝐴 +s 𝑚 ) <s ( 𝐴 +s 𝐵 ) ) )
276 273 275 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝐴 +s 𝑚 ) <s ( 𝐴 +s 𝐵 ) )
277 breq1 ⊢ ( 𝑎 = ( 𝐴 +s 𝑚 ) → ( 𝑎 <s ( 𝐴 +s 𝐵 ) ↔ ( 𝐴 +s 𝑚 ) <s ( 𝐴 +s 𝐵 ) ) )
278 276 277 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑎 = ( 𝐴 +s 𝑚 ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
279 278 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
280 262 279 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ 𝐿 𝑎 = ( 𝑙 +s 𝐵 ) ∨ ∃ 𝑚 ∈ 𝑀 𝑎 = ( 𝐴 +s 𝑚 ) ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
281 245 280 biimtrid ⊢ ( 𝜑 → ( 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) → 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
282 281 imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ) → 𝑎 <s ( 𝐴 +s 𝐵 ) )
283 breq2 ⊢ ( 𝑏 = ( 𝐴 +s 𝐵 ) → ( 𝑎 <s 𝑏 ↔ 𝑎 <s ( 𝐴 +s 𝐵 ) ) )
284 282 283 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ) → ( 𝑏 = ( 𝐴 +s 𝐵 ) → 𝑎 <s 𝑏 ) )
285 235 284 biimtrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ) → ( 𝑏 ∈ { ( 𝐴 +s 𝐵 ) } → 𝑎 <s 𝑏 ) )
286 285 3impia ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) ∧ 𝑏 ∈ { ( 𝐴 +s 𝐵 ) } ) → 𝑎 <s 𝑏 )
287 215 217 232 234 286 sltsd ⊢ ( 𝜑 → ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) <<s { ( 𝐴 +s 𝐵 ) } )
288 10 sneqd ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } = { ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) } )
289 287 288 breqtrd ⊢ ( 𝜑 → ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) <<s { ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) } )
290 eqid ⊢ ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) = ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) )
291 290 rnmpt ⊢ ran ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) = { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) }
292 sltsex2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
293 1 292 syl ⊢ ( 𝜑 → 𝑅 ∈ V )
294 293 mptexd ⊢ ( 𝜑 → ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) ∈ V )
295 rnexg ⊢ ( ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) ∈ V → ran ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) ∈ V )
296 294 295 syl ⊢ ( 𝜑 → ran ( 𝑟 ∈ 𝑅 ↦ ( 𝑟 +s 𝐵 ) ) ∈ V )
297 291 296 eqeltrrid ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∈ V )
298 eqid ⊢ ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) = ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) )
299 298 rnmpt ⊢ ran ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) = { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) }
300 sltsex2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ∈ V )
301 2 300 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
302 301 mptexd ⊢ ( 𝜑 → ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) ∈ V )
303 rnexg ⊢ ( ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) ∈ V → ran ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) ∈ V )
304 302 303 syl ⊢ ( 𝜑 → ran ( 𝑠 ∈ 𝑆 ↦ ( 𝐴 +s 𝑠 ) ) ∈ V )
305 299 304 eqeltrrid ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ∈ V )
306 297 305 unexd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ∈ V )
307 111 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ No )
308 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐵 ∈ No )
309 307 308 addscld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 +s 𝐵 ) ∈ No )
310 eleq1 ⊢ ( 𝑤 = ( 𝑟 +s 𝐵 ) → ( 𝑤 ∈ No ↔ ( 𝑟 +s 𝐵 ) ∈ No ) )
311 309 310 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝑤 = ( 𝑟 +s 𝐵 ) → 𝑤 ∈ No ) )
312 311 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) → 𝑤 ∈ No ) )
313 312 abssdv ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ⊆ No )
314 6 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝐴 ∈ No )
315 141 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ No )
316 314 315 addscld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝐴 +s 𝑠 ) ∈ No )
317 eleq1 ⊢ ( 𝑡 = ( 𝐴 +s 𝑠 ) → ( 𝑡 ∈ No ↔ ( 𝐴 +s 𝑠 ) ∈ No ) )
318 316 317 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑡 = ( 𝐴 +s 𝑠 ) → 𝑡 ∈ No ) )
319 318 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) → 𝑡 ∈ No ) )
320 319 abssdv ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ⊆ No )
321 313 320 unssd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ⊆ No )
322 velsn ⊢ ( 𝑎 ∈ { ( 𝐴 +s 𝐵 ) } ↔ 𝑎 = ( 𝐴 +s 𝐵 ) )
323 elun ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ↔ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) )
324 vex ⊢ 𝑏 ∈ V
325 324 122 elab ⊢ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ↔ ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) )
326 324 152 elab ⊢ ( 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ↔ ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) )
327 325 326 orbi12i ⊢ ( ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∨ ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ) )
328 323 327 bitri ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∨ ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ) )
329 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐴 = ( 𝐿 |s 𝑅 ) )
330 247 simp3d ⊢ ( 𝜑 → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
331 330 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
332 252 a1i ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐿 |s 𝑅 ) ∈ { ( 𝐿 |s 𝑅 ) } )
333 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ 𝑅 )
334 331 332 333 sltssepcd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐿 |s 𝑅 ) <s 𝑟 )
335 329 334 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐴 <s 𝑟 )
336 6 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝐴 ∈ No )
337 336 307 308 ltadds1d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐴 <s 𝑟 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝑟 +s 𝐵 ) ) )
338 335 337 mpbid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐴 +s 𝐵 ) <s ( 𝑟 +s 𝐵 ) )
339 breq2 ⊢ ( 𝑏 = ( 𝑟 +s 𝐵 ) → ( ( 𝐴 +s 𝐵 ) <s 𝑏 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝑟 +s 𝐵 ) ) )
340 338 339 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝑏 = ( 𝑟 +s 𝐵 ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
341 340 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
342 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝐵 = ( 𝑀 |s 𝑆 ) )
343 264 simp3d ⊢ ( 𝜑 → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
344 343 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
345 269 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑀 |s 𝑆 ) ∈ { ( 𝑀 |s 𝑆 ) } )
346 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 )
347 344 345 346 sltssepcd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑀 |s 𝑆 ) <s 𝑠 )
348 342 347 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝐵 <s 𝑠 )
349 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝐵 ∈ No )
350 349 315 314 ltadds2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝐵 <s 𝑠 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝐴 +s 𝑠 ) ) )
351 348 350 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝐴 +s 𝐵 ) <s ( 𝐴 +s 𝑠 ) )
352 breq2 ⊢ ( 𝑏 = ( 𝐴 +s 𝑠 ) → ( ( 𝐴 +s 𝐵 ) <s 𝑏 ↔ ( 𝐴 +s 𝐵 ) <s ( 𝐴 +s 𝑠 ) ) )
353 351 352 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑏 = ( 𝐴 +s 𝑠 ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
354 353 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
355 341 354 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑟 ∈ 𝑅 𝑏 = ( 𝑟 +s 𝐵 ) ∨ ∃ 𝑠 ∈ 𝑆 𝑏 = ( 𝐴 +s 𝑠 ) ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
356 328 355 biimtrid ⊢ ( 𝜑 → ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
357 356 imp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) → ( 𝐴 +s 𝐵 ) <s 𝑏 )
358 breq1 ⊢ ( 𝑎 = ( 𝐴 +s 𝐵 ) → ( 𝑎 <s 𝑏 ↔ ( 𝐴 +s 𝐵 ) <s 𝑏 ) )
359 357 358 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) → ( 𝑎 = ( 𝐴 +s 𝐵 ) → 𝑎 <s 𝑏 ) )
360 359 ex ⊢ ( 𝜑 → ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → ( 𝑎 = ( 𝐴 +s 𝐵 ) → 𝑎 <s 𝑏 ) ) )
361 360 com23 ⊢ ( 𝜑 → ( 𝑎 = ( 𝐴 +s 𝐵 ) → ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → 𝑎 <s 𝑏 ) ) )
362 322 361 biimtrid ⊢ ( 𝜑 → ( 𝑎 ∈ { ( 𝐴 +s 𝐵 ) } → ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) → 𝑎 <s 𝑏 ) ) )
363 362 3imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { ( 𝐴 +s 𝐵 ) } ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 )
364 217 306 234 321 363 sltsd ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) )
365 288 364 eqbrtrrd ⊢ ( 𝜑 → { ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) )
366 18 108 198 289 365 cofcut1d ⊢ ( 𝜑 → ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑝 +s 𝐵 ) } ∪ { 𝑏 ∣ ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑏 = ( 𝐴 +s 𝑞 ) } ) |s ( { 𝑐 ∣ ∃ 𝑒 ∈ ( R ‘ 𝐴 ) 𝑐 = ( 𝑒 +s 𝐵 ) } ∪ { 𝑑 ∣ ∃ 𝑓 ∈ ( R ‘ 𝐵 ) 𝑑 = ( 𝐴 +s 𝑓 ) } ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )
367 10 366 eqtrd ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )