Theorem addsov

Description: The value of surreal addition. Definition from Conway p. 5. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addsov	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-adds	⊢ +s = norec2 ( ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) )
2	1	norec2ov	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) )
3		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
4		addsfn	⊢ +s Fn ( No × No )
5		fnfun	⊢ ( +s Fn ( No × No ) → Fun +s )
6	4 5	ax-mp	⊢ Fun +s
7		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
8		fvex	⊢ ( R ‘ 𝐴 ) ∈ V
9	7 8	unex	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∈ V
10		snex	⊢ { 𝐴 } ∈ V
11	9 10	unex	⊢ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) ∈ V
12		fvex	⊢ ( L ‘ 𝐵 ) ∈ V
13		fvex	⊢ ( R ‘ 𝐵 ) ∈ V
14	12 13	unex	⊢ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∈ V
15		snex	⊢ { 𝐵 } ∈ V
16	14 15	unex	⊢ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ∈ V
17	11 16	xpex	⊢ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∈ V
18	17	difexi	⊢ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ∈ V
19		resfunexg	⊢ ( ( Fun +s ∧ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ∈ V ) → ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∈ V )
20	6 18 19	mp2an	⊢ ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∈ V
21		2fveq3	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( L ‘ ( 1st ‘ 𝑥 ) ) = ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
22		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
23	22	oveq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
24	23	eqeq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) ↔ 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
25	21 24	rexeqbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) ↔ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
26	25	abbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } )
27		2fveq3	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( L ‘ ( 2nd ‘ 𝑥 ) ) = ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
28		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
29	28	oveq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) )
30	29	eqeq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) ↔ 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) ) )
31	27 30	rexeqbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) ) )
32	31	abbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } = { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } )
33	26 32	uneq12d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } ) )
34		2fveq3	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( R ‘ ( 1st ‘ 𝑥 ) ) = ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
35	22	oveq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
36	35	eqeq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) ↔ 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
37	34 36	rexeqbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) ↔ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
38	37	abbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } )
39		2fveq3	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( R ‘ ( 2nd ‘ 𝑥 ) ) = ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
40	28	oveq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) )
41	40	eqeq2d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) ↔ 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) ) )
42	39 41	rexeqbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) ) )
43	42	abbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } = { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } )
44	38 43	uneq12d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) = ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } ) )
45	33 44	oveq12d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } ) ) )
46		oveq	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
47	46	eqeq2d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
48	47	rexbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
49	48	abbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } )
50		oveq	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) )
51	50	eqeq2d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) ↔ 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ) )
52	51	rexbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ) )
53	52	abbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } = { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } )
54	49 53	uneq12d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) )
55		oveq	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
56	55	eqeq2d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
57	56	rexbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
58	57	abbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } )
59		oveq	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) )
60	59	eqeq2d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) ↔ 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ) )
61	60	rexbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ) )
62	61	abbidv	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } = { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } )
63	58 62	uneq12d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } ) = ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) )
64	54 63	oveq12d	⊢ ( 𝑎 = ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝑎 𝑟 ) } ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) ) )
65		eqid	⊢ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) = ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) )
66		ovex	⊢ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) ) ∈ V
67	45 64 65 66	ovmpo	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) ) )
68	3 20 67	mp2an	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) )
69		op1stg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
70	69	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( L ‘ 𝐴 ) )
71	70	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑙 ∈ ( L ‘ 𝐴 ) ) )
72		op2ndg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
73	72	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
74	73	oveq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) )
75		elun1	⊢ ( 𝑙 ∈ ( L ‘ 𝐴 ) → 𝑙 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
76		elun1	⊢ ( 𝑙 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
77	75 76	syl	⊢ ( 𝑙 ∈ ( L ‘ 𝐴 ) → 𝑙 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
78	77	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
79		snidg	⊢ ( 𝐵 ∈ No → 𝐵 ∈ { 𝐵 } )
80		elun2	⊢ ( 𝐵 ∈ { 𝐵 } → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
81	79 80	syl	⊢ ( 𝐵 ∈ No → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
82	81	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
83	82	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
84	78 83	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ⟨ 𝑙 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
85		leftirr	⊢ ( 𝐴 ∈ No → ¬ 𝐴 ∈ ( L ‘ 𝐴 ) )
86	85	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐴 ∈ ( L ‘ 𝐴 ) )
87		eleq1	⊢ ( 𝑙 = 𝐴 → ( 𝑙 ∈ ( L ‘ 𝐴 ) ↔ 𝐴 ∈ ( L ‘ 𝐴 ) ) )
88	87	notbid	⊢ ( 𝑙 = 𝐴 → ( ¬ 𝑙 ∈ ( L ‘ 𝐴 ) ↔ ¬ 𝐴 ∈ ( L ‘ 𝐴 ) ) )
89	86 88	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 = 𝐴 → ¬ 𝑙 ∈ ( L ‘ 𝐴 ) ) )
90	89	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ 𝐴 ) → 𝑙 ≠ 𝐴 ) )
91	90	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → 𝑙 ≠ 𝐴 )
92	91	orcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) )
93		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → 𝑙 ∈ ( L ‘ 𝐴 ) )
94		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → 𝐵 ∈ No )
95		opthneg	⊢ ( ( 𝑙 ∈ ( L ‘ 𝐴 ) ∧ 𝐵 ∈ No ) → ( ⟨ 𝑙 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
96	93 94 95	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( ⟨ 𝑙 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
97	92 96	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ⟨ 𝑙 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
98		eldifsn	⊢ ( ⟨ 𝑙 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝑙 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝑙 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
99	84 97 98	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ⟨ 𝑙 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
100	99	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑙 , 𝐵 ⟩ ) = ( +s ‘ ⟨ 𝑙 , 𝐵 ⟩ ) )
101		df-ov	⊢ ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑙 , 𝐵 ⟩ )
102		df-ov	⊢ ( 𝑙 +s 𝐵 ) = ( +s ‘ ⟨ 𝑙 , 𝐵 ⟩ )
103	100 101 102	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( 𝑙 +s 𝐵 ) )
104	74 103	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑙 +s 𝐵 ) )
105	104	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐴 ) ) → ( 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) )
106	105	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ 𝐴 ) → ( 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) ) )
107	71 106	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) ) )
108	107	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) )
109	70 108	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) ) )
110	109	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } )
111	72	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( L ‘ 𝐵 ) )
112	111	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑙 ∈ ( L ‘ 𝐵 ) ) )
113	69	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
114	113	oveq1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) )
115		snidg	⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
116	115	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ { 𝐴 } )
117		elun2	⊢ ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
118	116 117	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
119	118	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
120		elun1	⊢ ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
121		elun1	⊢ ( 𝑙 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
122	120 121	syl	⊢ ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
123	122	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
124	119 123	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
125		leftirr	⊢ ( 𝐵 ∈ No → ¬ 𝐵 ∈ ( L ‘ 𝐵 ) )
126	125	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐵 ∈ ( L ‘ 𝐵 ) )
127		eleq1	⊢ ( 𝑙 = 𝐵 → ( 𝑙 ∈ ( L ‘ 𝐵 ) ↔ 𝐵 ∈ ( L ‘ 𝐵 ) ) )
128	127	notbid	⊢ ( 𝑙 = 𝐵 → ( ¬ 𝑙 ∈ ( L ‘ 𝐵 ) ↔ ¬ 𝐵 ∈ ( L ‘ 𝐵 ) ) )
129	126 128	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 = 𝐵 → ¬ 𝑙 ∈ ( L ‘ 𝐵 ) ) )
130	129	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ≠ 𝐵 ) )
131	130	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝑙 ≠ 𝐵 )
132	131	olcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) )
133		opthneg	⊢ ( ( 𝐴 ∈ No ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) ) )
134	133	adantlr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) ) )
135	132 134	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
136		eldifsn	⊢ ( ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
137	124 135 136	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
138	137	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑙 ⟩ ) = ( +s ‘ ⟨ 𝐴 , 𝑙 ⟩ ) )
139		df-ov	⊢ ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑙 ⟩ )
140		df-ov	⊢ ( 𝐴 +s 𝑙 ) = ( +s ‘ ⟨ 𝐴 , 𝑙 ⟩ )
141	138 139 140	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 +s 𝑙 ) )
142	114 141	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 +s 𝑙 ) )
143	142	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) )
144	143	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ 𝐵 ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) ) )
145	112 144	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) ) )
146	145	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) )
147	111 146	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) ) )
148	147	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } = { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } )
149	110 148	uneq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) )
150	69	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( R ‘ 𝐴 ) )
151	150	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑟 ∈ ( R ‘ 𝐴 ) ) )
152	72	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
153	152	oveq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) )
154		elun2	⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
155		elun1	⊢ ( 𝑟 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
156	154 155	syl	⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
157	156	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
158	82	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
159	157 158	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
160		rightirr	⊢ ( 𝐴 ∈ No → ¬ 𝐴 ∈ ( R ‘ 𝐴 ) )
161	160	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐴 ∈ ( R ‘ 𝐴 ) )
162		eleq1	⊢ ( 𝑟 = 𝐴 → ( 𝑟 ∈ ( R ‘ 𝐴 ) ↔ 𝐴 ∈ ( R ‘ 𝐴 ) ) )
163	162	notbid	⊢ ( 𝑟 = 𝐴 → ( ¬ 𝑟 ∈ ( R ‘ 𝐴 ) ↔ ¬ 𝐴 ∈ ( R ‘ 𝐴 ) ) )
164	161 163	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 = 𝐴 → ¬ 𝑟 ∈ ( R ‘ 𝐴 ) ) )
165	164	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ≠ 𝐴 ) )
166	165	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ≠ 𝐴 )
167	166	orcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) )
168		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
169		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝐵 ∈ No )
170		opthneg	⊢ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝐵 ∈ No ) → ( ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
171	168 169 170	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
172	167 171	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
173		eldifsn	⊢ ( ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
174	159 172 173	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
175	174	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑟 , 𝐵 ⟩ ) = ( +s ‘ ⟨ 𝑟 , 𝐵 ⟩ ) )
176		df-ov	⊢ ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑟 , 𝐵 ⟩ )
177		df-ov	⊢ ( 𝑟 +s 𝐵 ) = ( +s ‘ ⟨ 𝑟 , 𝐵 ⟩ )
178	175 176 177	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( 𝑟 +s 𝐵 ) )
179	153 178	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑟 +s 𝐵 ) )
180	179	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) )
181	180	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐴 ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) ) )
182	151 181	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) ) )
183	182	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) )
184	150 183	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) ) )
185	184	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } )
186	72	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( R ‘ 𝐵 ) )
187	186	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑟 ∈ ( R ‘ 𝐵 ) ) )
188	69	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
189	188	oveq1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) )
190	116	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝐴 ∈ { 𝐴 } )
191	190 117	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
192		elun2	⊢ ( 𝑟 ∈ ( R ‘ 𝐵 ) → 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
193	192	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
194		elun1	⊢ ( 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
195	193 194	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
196	191 195	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
197		rightirr	⊢ ( 𝐵 ∈ No → ¬ 𝐵 ∈ ( R ‘ 𝐵 ) )
198	197	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐵 ∈ ( R ‘ 𝐵 ) )
199		eleq1	⊢ ( 𝑟 = 𝐵 → ( 𝑟 ∈ ( R ‘ 𝐵 ) ↔ 𝐵 ∈ ( R ‘ 𝐵 ) ) )
200	199	notbid	⊢ ( 𝑟 = 𝐵 → ( ¬ 𝑟 ∈ ( R ‘ 𝐵 ) ↔ ¬ 𝐵 ∈ ( R ‘ 𝐵 ) ) )
201	198 200	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 = 𝐵 → ¬ 𝑟 ∈ ( R ‘ 𝐵 ) ) )
202	201	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐵 ) → 𝑟 ≠ 𝐵 ) )
203	202	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ≠ 𝐵 )
204	203	olcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) )
205		opthneg	⊢ ( ( 𝐴 ∈ No ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) ) )
206	205	adantlr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) ) )
207	204 206	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
208		eldifsn	⊢ ( ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
209	196 207 208	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
210	209	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑟 ⟩ ) = ( +s ‘ ⟨ 𝐴 , 𝑟 ⟩ ) )
211		df-ov	⊢ ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑟 ⟩ )
212		df-ov	⊢ ( 𝐴 +s 𝑟 ) = ( +s ‘ ⟨ 𝐴 , 𝑟 ⟩ )
213	210 211 212	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 +s 𝑟 ) )
214	189 213	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 +s 𝑟 ) )
215	214	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) )
216	215	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐵 ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) ) )
217	187 216	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) ) )
218	217	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) )
219	186 218	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) ) )
220	219	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } = { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } )
221	185 220	uneq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) = ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) )
222	149 221	oveq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) ) )
223	68 222	syl5eq	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ⟨ 𝐴 , 𝐵 ⟩ ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) ) )
224	2 223	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) ) )