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