Theorem dfaddc2 4382

Description: Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)

Assertion

Ref	Expression
dfaddc2	|- (A +o B) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA)

Proof of Theorem dfaddc2

Dummy variables x y z t w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-addc 4379	. 2 |- (A +o B) = {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}
2		vex 2863	. . . . 5 |- x e. _V
3	2	elimak 4260	. . . 4 |- (x e. ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA) <-> E.y e. A <<y, x>> e. (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B))
4		opkex 4114	. . . . . . 7 |- <<y, x>> e. _V
5	4	elimak 4260	. . . . . 6 |- (<<y, x>> e. (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B) <-> E.t e. ~P1 ~P1 B<<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)))
6		elpw12 4146	. . . . . . . . . 10 |- (t e. ~P1 ~P1 B <-> E.z e. B t = {{z}})
7	6	anbi1i 676	. . . . . . . . 9 |- ((t e. ~P1 ~P1 B /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> (E.z e. B t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
8		r19.41v 2765	. . . . . . . . 9 |- (E.z e. B (t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> (E.z e. B t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
9	7, 8	bitr4i 243	. . . . . . . 8 |- ((t e. ~P1 ~P1 B /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.z e. B (t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
10	9	exbii 1582	. . . . . . 7 |- (E.t(t e. ~P1 ~P1 B /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.z e. B (t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
11		df-rex 2621	. . . . . . 7 |- (E.t e. ~P1 ~P1 B<<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 B /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
12		rexcom4 2879	. . . . . . 7 |- (E.z e. B E.t(t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.z e. B (t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
13	10, 11, 12	3bitr4i 268	. . . . . 6 |- (E.t e. ~P1 ~P1 B<<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.z e. B E.t(t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
14		snex 4112	. . . . . . . . 9 |- {{z}} e. _V
15		opkeq1 4060	. . . . . . . . . 10 |- (t = {{z}} -> <<t, <<y, x>>>> = <<{{z}}, <<y, x>>>>)
16	15	eleq1d 2419	. . . . . . . . 9 |- (t = {{z}} -> (<<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) <-> <<{{z}}, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))))
17	14, 16	ceqsexv 2895	. . . . . . . 8 |- (E.t(t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> <<{{z}}, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)))
18		eldif 3222	. . . . . . . 8 |- (<<{{z}}, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (<<{{z}}, <<y, x>>>> e. Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ -. <<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)))
19		opkex 4114	. . . . . . . . . . . 12 |- <<z, y>> e. _V
20	19	elcompl 3226	. . . . . . . . . . 11 |- (<<z, y>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. <<z, y>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
21		vex 2863	. . . . . . . . . . . . 13 |- z e. _V
22		vex 2863	. . . . . . . . . . . . 13 |- y e. _V
23	21, 22	ndisjrelk 4324	. . . . . . . . . . . 12 |- (<<z, y>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (z i^i y) =/= (/))
24	23	necon2bbii 2573	. . . . . . . . . . 11 |- ((z i^i y) = (/) <-> -. <<z, y>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
25	20, 24	bitr4i 243	. . . . . . . . . 10 |- (<<z, y>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (z i^i y) = (/))
26	21, 22, 2	otkelins3k 4257	. . . . . . . . . 10 |- (<<{{z}}, <<y, x>>>> e. Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<z, y>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
27		incom 3449	. . . . . . . . . . 11 |- (y i^i z) = (z i^i y)
28	27	eqeq1i 2360	. . . . . . . . . 10 |- ((y i^i z) = (/) <-> (z i^i y) = (/))
29	25, 26, 28	3bitr4i 268	. . . . . . . . 9 |- (<<{{z}}, <<y, x>>>> e. Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (y i^i z) = (/))
30		dfcleq 2347	. . . . . . . . . 10 |- (x = (y u. z) <-> A.w(w e. x <-> w e. (y u. z)))
31		opkex 4114	. . . . . . . . . . . . . 14 |- <<{{z}}, <<y, x>>>> e. _V
32	31	elimak 4260	. . . . . . . . . . . . 13 |- (<<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )))
33		df-rex 2621	. . . . . . . . . . . . 13 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
34		elpw141c 4151	. . . . . . . . . . . . . . . . 17 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.w t = {{{{{w}}}}})
35	34	anbi1i 676	. . . . . . . . . . . . . . . 16 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> (E.w t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
36		19.41v 1901	. . . . . . . . . . . . . . . 16 |- (E.w(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> (E.w t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
37	35, 36	bitr4i 243	. . . . . . . . . . . . . . 15 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> E.w(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
38	37	exbii 1582	. . . . . . . . . . . . . 14 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> E.tE.w(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
39		excom 1741	. . . . . . . . . . . . . 14 |- (E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> E.tE.w(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
40	38, 39	bitr4i 243	. . . . . . . . . . . . 13 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
41	32, 33, 40	3bitri 262	. . . . . . . . . . . 12 |- (<<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
42		snex 4112	. . . . . . . . . . . . . . 15 |- {{{{{w}}}}} e. _V
43		opkeq1 4060	. . . . . . . . . . . . . . . 16 |- (t = {{{{{w}}}}} -> <<t, <<{{z}}, <<y, x>>>>>> = <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>>)
44	43	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (t = {{{{{w}}}}} -> (<<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )) <-> <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))))
45	42, 44	ceqsexv 2895	. . . . . . . . . . . . . 14 |- (E.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )))
46		elsymdif 3224	. . . . . . . . . . . . . 14 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )) <-> -. (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins2k Sk <-> <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )))
47		snex 4112	. . . . . . . . . . . . . . . . . 18 |- {{{w}}} e. _V
48	47, 14, 4	otkelins2k 4256	. . . . . . . . . . . . . . . . 17 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins2k Sk <-> <<{{{w}}}, <<y, x>>>> e. Ins2k Sk )
49		snex 4112	. . . . . . . . . . . . . . . . . 18 |- {w} e. _V
50	49, 22, 2	otkelins2k 4256	. . . . . . . . . . . . . . . . 17 |- (<<{{{w}}}, <<y, x>>>> e. Ins2k Sk <-> <<{w}, x>> e. Sk )
51		vex 2863	. . . . . . . . . . . . . . . . . 18 |- w e. _V
52	51, 2	elssetk 4271	. . . . . . . . . . . . . . . . 17 |- (<<{w}, x>> e. Sk <-> w e. x)
53	48, 50, 52	3bitri 262	. . . . . . . . . . . . . . . 16 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins2k Sk <-> w e. x)
54	47, 14, 4	otkelins2k 4256	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins3k Sk <-> <<{{{w}}}, <<y, x>>>> e. Ins3k Sk )
55	49, 22, 2	otkelins3k 4257	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{w}}}, <<y, x>>>> e. Ins3k Sk <-> <<{w}, y>> e. Sk )
56	51, 22	elssetk 4271	. . . . . . . . . . . . . . . . . . 19 |- (<<{w}, y>> e. Sk <-> w e. y)
57	54, 55, 56	3bitri 262	. . . . . . . . . . . . . . . . . 18 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins3k Sk <-> w e. y)
58	47, 14, 4	otkelins3k 4257	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins3k SIk SIk Sk <-> <<{{{w}}}, {{z}}>> e. SIk SIk Sk )
59		snex 4112	. . . . . . . . . . . . . . . . . . . 20 |- {{w}} e. _V
60		snex 4112	. . . . . . . . . . . . . . . . . . . 20 |- {z} e. _V
61	59, 60	opksnelsik 4266	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{w}}}, {{z}}>> e. SIk SIk Sk <-> <<{{w}}, {z}>> e. SIk Sk )
62	49, 21	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{w}}, {z}>> e. SIk Sk <-> <<{w}, z>> e. Sk )
63	51, 21	elssetk 4271	. . . . . . . . . . . . . . . . . . . 20 |- (<<{w}, z>> e. Sk <-> w e. z)
64	62, 63	bitri 240	. . . . . . . . . . . . . . . . . . 19 |- (<<{{w}}, {z}>> e. SIk Sk <-> w e. z)
65	58, 61, 64	3bitri 262	. . . . . . . . . . . . . . . . . 18 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins3k SIk SIk Sk <-> w e. z)
66	57, 65	orbi12i 507	. . . . . . . . . . . . . . . . 17 |- ((<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins3k Sk \/ <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins3k SIk SIk Sk ) <-> (w e. y \/ w e. z))
67		elun 3221	. . . . . . . . . . . . . . . . 17 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ) <-> (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins3k Sk \/ <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins3k SIk SIk Sk ))
68		elun 3221	. . . . . . . . . . . . . . . . 17 |- (w e. (y u. z) <-> (w e. y \/ w e. z))
69	66, 67, 68	3bitr4i 268	. . . . . . . . . . . . . . . 16 |- (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ) <-> w e. (y u. z))
70	53, 69	bibi12i 306	. . . . . . . . . . . . . . 15 |- ((<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins2k Sk <-> <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )) <-> (w e. x <-> w e. (y u. z)))
71	70	notbii 287	. . . . . . . . . . . . . 14 |- (-. (<<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. Ins2k Ins2k Sk <-> <<{{{{{w}}}}}, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk )) <-> -. (w e. x <-> w e. (y u. z)))
72	45, 46, 71	3bitri 262	. . . . . . . . . . . . 13 |- (E.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> -. (w e. x <-> w e. (y u. z)))
73	72	exbii 1582	. . . . . . . . . . . 12 |- (E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{z}}, <<y, x>>>>>> e. ( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))) <-> E.w -. (w e. x <-> w e. (y u. z)))
74		exnal 1574	. . . . . . . . . . . 12 |- (E.w -. (w e. x <-> w e. (y u. z)) <-> -. A.w(w e. x <-> w e. (y u. z)))
75	41, 73, 74	3bitri 262	. . . . . . . . . . 11 |- (<<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c) <-> -. A.w(w e. x <-> w e. (y u. z)))
76	75	con2bii 322	. . . . . . . . . 10 |- (A.w(w e. x <-> w e. (y u. z)) <-> -. <<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))
77	30, 76	bitr2i 241	. . . . . . . . 9 |- (-. <<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c) <-> x = (y u. z))
78	29, 77	anbi12i 678	. . . . . . . 8 |- ((<<{{z}}, <<y, x>>>> e. Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ -. <<{{z}}, <<y, x>>>> e. (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) <-> ((y i^i z) = (/) /\ x = (y u. z)))
79	17, 18, 78	3bitri 262	. . . . . . 7 |- (E.t(t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> ((y i^i z) = (/) /\ x = (y u. z)))
80	79	rexbii 2640	. . . . . 6 |- (E.z e. B E.t(t = {{z}} /\ <<t, <<y, x>>>> e. ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.z e. B ((y i^i z) = (/) /\ x = (y u. z)))
81	5, 13, 80	3bitri 262	. . . . 5 |- (<<y, x>> e. (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B) <-> E.z e. B ((y i^i z) = (/) /\ x = (y u. z)))
82	81	rexbii 2640	. . . 4 |- (E.y e. A <<y, x>> e. (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B) <-> E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z)))
83	3, 82	bitri 240	. . 3 |- (x e. ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA) <-> E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z)))
84	83	abbi2i 2465	. 2 |- ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA) = {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}
85	1, 84	eqtr4i 2376	1 |- (A +o B) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA)

Syntax hints:  -. wn 3   <-> wb 176   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  E.wrex 2616   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   i^i cin 3209   (+) csymdif 3210  (/)c0 3551  {csn 3738  <<copk 4058  1_cc1c 4135  ~P₁ cpw1 4136   Ins2_k cins2k 4177   Ins3_k cins3k 4178  "_kcimak 4180   SI_k csik 4182   S_k cssetk 4184   +o cplc 4376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-rex 2621  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-pw 3725  df-sn 3742  df-pr 3743  df-opk 4059  df-1c 4137  df-pw1 4138  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-sik 4193  df-ssetk 4194  df-addc 4379

This theorem is referenced by:  addceq1  4384  addceq2  4385  addcexg  4394  dfnnc2  4396  nnc0suc  4413  nncaddccl  4420  nnsucelrlem1  4425  preaddccan2lem1  4455  ltfinex  4465  evenodddisjlem1  4516  dfphi2  4570  phialllem1  4617