Theorem addsval

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

	Ref	Expression
Assertion	addsval	⊢ ( ( 𝐴 ∈ 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	⊢ ¬ 𝐴 ∈ ( L ‘ 𝐴 )
86	85	a1i	⊢ ( ( 𝐴 ∈ 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	71 105	sylbida	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) )
107	70 106	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) ) )
108	107	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } )
109	72	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( L ‘ 𝐵 ) )
110	109	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑙 ∈ ( L ‘ 𝐵 ) ) )
111	69	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
112	111	oveq1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) )
113		snidg	⊢ ( 𝐴 ∈ No → 𝐴 ∈ { 𝐴 } )
114	113	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ { 𝐴 } )
115		elun2	⊢ ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
116	114 115	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
117	116	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
118		elun1	⊢ ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
119		elun1	⊢ ( 𝑙 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
120	118 119	syl	⊢ ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
121	120	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝑙 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
122	117 121	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
123		leftirr	⊢ ¬ 𝐵 ∈ ( L ‘ 𝐵 )
124	123	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐵 ∈ ( L ‘ 𝐵 ) )
125		eleq1	⊢ ( 𝑙 = 𝐵 → ( 𝑙 ∈ ( L ‘ 𝐵 ) ↔ 𝐵 ∈ ( L ‘ 𝐵 ) ) )
126	125	notbid	⊢ ( 𝑙 = 𝐵 → ( ¬ 𝑙 ∈ ( L ‘ 𝐵 ) ↔ ¬ 𝐵 ∈ ( L ‘ 𝐵 ) ) )
127	124 126	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 = 𝐵 → ¬ 𝑙 ∈ ( L ‘ 𝐵 ) ) )
128	127	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑙 ∈ ( L ‘ 𝐵 ) → 𝑙 ≠ 𝐵 ) )
129	128	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → 𝑙 ≠ 𝐵 )
130	129	olcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) )
131		opthneg	⊢ ( ( 𝐴 ∈ No ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) ) )
132	131	adantlr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵 ) ) )
133	130 132	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
134		eldifsn	⊢ ( ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝐴 , 𝑙 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
135	122 133 134	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑙 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
136	135	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑙 ⟩ ) = ( +s ‘ ⟨ 𝐴 , 𝑙 ⟩ ) )
137		df-ov	⊢ ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑙 ⟩ )
138		df-ov	⊢ ( 𝐴 +s 𝑙 ) = ( +s ‘ ⟨ 𝐴 , 𝑙 ⟩ )
139	136 137 138	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 +s 𝑙 ) )
140	112 139	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) = ( 𝐴 +s 𝑙 ) )
141	140	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ 𝐵 ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) )
142	110 141	sylbida	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ 𝑧 = ( 𝐴 +s 𝑙 ) ) )
143	109 142	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) ) )
144	143	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } = { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } )
145	108 144	uneq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑙 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑙 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) )
146	69	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( R ‘ 𝐴 ) )
147	146	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑟 ∈ ( R ‘ 𝐴 ) ) )
148	72	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
149	148	oveq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) )
150		elun2	⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
151		elun1	⊢ ( 𝑟 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
152	150 151	syl	⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
153	152	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
154	82	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝐵 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
155	153 154	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
156		rightirr	⊢ ¬ 𝐴 ∈ ( R ‘ 𝐴 )
157	156	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐴 ∈ ( R ‘ 𝐴 ) )
158		eleq1	⊢ ( 𝑟 = 𝐴 → ( 𝑟 ∈ ( R ‘ 𝐴 ) ↔ 𝐴 ∈ ( R ‘ 𝐴 ) ) )
159	158	notbid	⊢ ( 𝑟 = 𝐴 → ( ¬ 𝑟 ∈ ( R ‘ 𝐴 ) ↔ ¬ 𝐴 ∈ ( R ‘ 𝐴 ) ) )
160	157 159	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 = 𝐴 → ¬ 𝑟 ∈ ( R ‘ 𝐴 ) ) )
161	160	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐴 ) → 𝑟 ≠ 𝐴 ) )
162	161	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ≠ 𝐴 )
163	162	orcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) )
164		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
165		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → 𝐵 ∈ No )
166		opthneg	⊢ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝐵 ∈ No ) → ( ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
167	164 165 166	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵 ) ) )
168	163 167	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
169		eldifsn	⊢ ( ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝑟 , 𝐵 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
170	155 168 169	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ⟨ 𝑟 , 𝐵 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
171	170	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑟 , 𝐵 ⟩ ) = ( +s ‘ ⟨ 𝑟 , 𝐵 ⟩ ) )
172		df-ov	⊢ ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝑟 , 𝐵 ⟩ )
173		df-ov	⊢ ( 𝑟 +s 𝐵 ) = ( +s ‘ ⟨ 𝑟 , 𝐵 ⟩ )
174	171 172 173	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝐵 ) = ( 𝑟 +s 𝐵 ) )
175	149 174	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑟 +s 𝐵 ) )
176	175	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐴 ) ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) )
177	147 176	sylbida	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑦 = ( 𝑟 +s 𝐵 ) ) )
178	146 177	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) ) )
179	178	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } = { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } )
180	72	fveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( R ‘ 𝐵 ) )
181	180	eleq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑟 ∈ ( R ‘ 𝐵 ) ) )
182	69	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
183	182	oveq1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) )
184	114	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝐴 ∈ { 𝐴 } )
185	184 115	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝐴 ∈ ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) )
186		elun2	⊢ ( 𝑟 ∈ ( R ‘ 𝐵 ) → 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
187	186	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
188		elun1	⊢ ( 𝑟 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
189	187 188	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ∈ ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) )
190	185 189	opelxpd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) )
191		rightirr	⊢ ¬ 𝐵 ∈ ( R ‘ 𝐵 )
192	191	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ¬ 𝐵 ∈ ( R ‘ 𝐵 ) )
193		eleq1	⊢ ( 𝑟 = 𝐵 → ( 𝑟 ∈ ( R ‘ 𝐵 ) ↔ 𝐵 ∈ ( R ‘ 𝐵 ) ) )
194	193	notbid	⊢ ( 𝑟 = 𝐵 → ( ¬ 𝑟 ∈ ( R ‘ 𝐵 ) ↔ ¬ 𝐵 ∈ ( R ‘ 𝐵 ) ) )
195	192 194	syl5ibrcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 = 𝐵 → ¬ 𝑟 ∈ ( R ‘ 𝐵 ) ) )
196	195	necon2ad	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑟 ∈ ( R ‘ 𝐵 ) → 𝑟 ≠ 𝐵 ) )
197	196	imp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → 𝑟 ≠ 𝐵 )
198	197	olcd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) )
199		opthneg	⊢ ( ( 𝐴 ∈ No ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) ) )
200	199	adantlr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵 ) ) )
201	198 200	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ )
202		eldifsn	⊢ ( ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ( ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∧ ⟨ 𝐴 , 𝑟 ⟩ ≠ ⟨ 𝐴 , 𝐵 ⟩ ) )
203	190 201 202	sylanbrc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ⟨ 𝐴 , 𝑟 ⟩ ∈ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
204	203	fvresd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑟 ⟩ ) = ( +s ‘ ⟨ 𝐴 , 𝑟 ⟩ ) )
205		df-ov	⊢ ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ‘ ⟨ 𝐴 , 𝑟 ⟩ )
206		df-ov	⊢ ( 𝐴 +s 𝑟 ) = ( +s ‘ ⟨ 𝐴 , 𝑟 ⟩ )
207	204 205 206	3eqtr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝐴 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 +s 𝑟 ) )
208	183 207	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) = ( 𝐴 +s 𝑟 ) )
209	208	eqeq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ 𝐵 ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) )
210	181 209	sylbida	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ 𝑧 = ( 𝐴 +s 𝑟 ) ) )
211	180 210	rexeqbidva	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) ) )
212	211	abbidv	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } = { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } )
213	179 212	uneq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑦 = ( 𝑟 ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) 𝑧 = ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ( +s ↾ ( ( ( ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∪ { 𝐴 } ) × ( ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ∪ { 𝐵 } ) ) ∖ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) 𝑟 ) } ) = ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) )
214	145 213	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 𝑟 ) } ) ) )
215	68 214	eqtrid	⊢ ( ( 𝐴 ∈ 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 𝑟 ) } ) ) )
216	2 215	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑦 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑟 ) } ) ) )