addsval

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

		Ref	Expression
	Assertion	addsval	$⊢ (A \in No \land B \in No) \to A +_{s} B = (\{y \| \exists l \in L (A) y = l +_{s} B\} \cup \{z \| \exists l \in L (B) z = A +_{s} l\}) \|_{s} (\{y \| \exists r \in R (A) y = r +_{s} B\} \cup \{z \| \exists r \in R (B) z = A +_{s} r\})$

Proof

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

Metamath Proof Explorer

Theorem addsval

Proof