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 𝑠 ) } ) ) )