Theorem evenodddisjlem1 4515

Description: Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)

Assertion

Ref	Expression
evenodddisjlem1	|- {j | ((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)))} e. _V

Distinct variable group:   j,n

Proof of Theorem evenodddisjlem1

Dummy variables x a b y t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-or 359	. . . 4 |- (((j +o j) = (/) \/ A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))) <-> (-. (j +o j) = (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))))
2		vex 2862	. . . . . 6 |- j e. _V
3	2	elimakv 4260	. . . . 5 |- (j e. (( ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i (({(/)} u. ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( ∼ Ins3k `'k SIk SIk SIk (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins2k Ins3k SIk SIk SIk Sk u. Ins3k SIk SIk SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i Ins3k Imagek(( 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 1c))"k~P1 1c) i^i Ins2k ( _I_kk \ ({(/)} X.k _V)))"k~P1 1c)"k Nn )) X.k _V))"k_V) <-> E.x<<x, j>> e. ( ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i (({(/)} u. ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( ∼ Ins3k `'k SIk SIk SIk (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins2k Ins3k SIk SIk SIk Sk u. Ins3k SIk SIk SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i Ins3k Imagek(( 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 1c))"k~P1 1c) i^i Ins2k ( _I_kk \ ({(/)} X.k _V)))"k~P1 1c)"k Nn )) X.k _V)))
4		elin 3219	. . . . . . 7 |- (<<x, j>> e. ( ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i (({(/)} u. ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( ∼ Ins3k `'k SIk SIk SIk (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins2k Ins3k SIk SIk SIk Sk u. Ins3k SIk SIk SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i Ins3k Imagek(( 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 1c))"k~P1 1c) i^i Ins2k ( _I_kk \ ({(/)} X.k _V)))"k~P1 1c)"k Nn )) X.k _V)) <-> (<<x, j>> e. ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) /\ <<x, j>> e. (({(/)} u. ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( ∼ Ins3k `'k SIk SIk SIk (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins2k Ins3k SIk SIk SIk Sk u. Ins3k SIk SIk SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) i^i Ins3k Imagek(( 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 1c))"k~P1 1c) i^i Ins2k ( _I_kk \ ({(/)} X.k _V)))"k~P1 1c)"k Nn )) X.k _V)))
5		opkex 4113	. . . . . . . . . . . . 13 |- <<x, j>> e. _V
6	5	elimak 4259	. . . . . . . . . . . 12 |- (<<x, j>> e. (( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)))
7		elpw121c 4148	. . . . . . . . . . . . . . . 16 |- (t e. ~P1 ~P1 1c <-> E.y t = {{{y}}})
8	7	anbi1i 676	. . . . . . . . . . . . . . 15 |- ((t e. ~P1 ~P1 1c /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> (E.y t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
9		19.41v 1901	. . . . . . . . . . . . . . 15 |- (E.y(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> (E.y t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
10	8, 9	bitr4i 243	. . . . . . . . . . . . . 14 |- ((t e. ~P1 ~P1 1c /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> E.y(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
11	10	exbii 1582	. . . . . . . . . . . . 13 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> E.tE.y(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
12		df-rex 2620	. . . . . . . . . . . . 13 |- (E.t e. ~P1 ~P1 1c<<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
13		excom 1741	. . . . . . . . . . . . 13 |- (E.yE.t(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> E.tE.y(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
14	11, 12, 13	3bitr4i 268	. . . . . . . . . . . 12 |- (E.t e. ~P1 ~P1 1c<<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> E.yE.t(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
15		snex 4111	. . . . . . . . . . . . . . 15 |- {{{y}}} e. _V
16		opkeq1 4059	. . . . . . . . . . . . . . . 16 |- (t = {{{y}}} -> <<t, <<x, j>>>> = <<{{{y}}}, <<x, j>>>>)
17	16	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (t = {{{y}}} -> (<<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> <<{{{y}}}, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))))
18	15, 17	ceqsexv 2894	. . . . . . . . . . . . . 14 |- (E.t(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> <<{{{y}}}, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)))
19		elsymdif 3223	. . . . . . . . . . . . . 14 |- (<<{{{y}}}, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> -. (<<{{{y}}}, <<x, j>>>> e. Ins3k Sk <-> <<{{{y}}}, <<x, j>>>> e. Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)))
20		snex 4111	. . . . . . . . . . . . . . . . . 18 |- {y} e. _V
21		vex 2862	. . . . . . . . . . . . . . . . . 18 |- x e. _V
22	20, 21, 2	otkelins3k 4256	. . . . . . . . . . . . . . . . 17 |- (<<{{{y}}}, <<x, j>>>> e. Ins3k Sk <-> <<{y}, x>> e. Sk )
23		vex 2862	. . . . . . . . . . . . . . . . . 18 |- y e. _V
24	23, 21	elssetk 4270	. . . . . . . . . . . . . . . . 17 |- (<<{y}, x>> e. Sk <-> y e. x)
25	22, 24	bitri 240	. . . . . . . . . . . . . . . 16 |- (<<{{{y}}}, <<x, j>>>> e. Ins3k Sk <-> y e. x)
26	20, 21, 2	otkelins2k 4255	. . . . . . . . . . . . . . . . 17 |- (<<{{{y}}}, <<x, j>>>> e. Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> <<{y}, j>> e. (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))
27		opkex 4113	. . . . . . . . . . . . . . . . . . . 20 |- <<{y}, j>> e. _V
28	27	elimak 4259	. . . . . . . . . . . . . . . . . . 19 |- (<<{y}, j>> e. (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
29		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t e. ~P1 ~P1 1c <-> E.b t = {{{b}}})
30	29	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> (E.b t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
31		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.b(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> (E.b t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
32	30, 31	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.b(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
33	32	exbii 1582	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.b(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
34		df-rex 2620	. . . . . . . . . . . . . . . . . . . 20 |- (E.t e. ~P1 ~P1 1c<<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
35		excom 1741	. . . . . . . . . . . . . . . . . . . 20 |- (E.bE.t(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.b(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
36	33, 34, 35	3bitr4i 268	. . . . . . . . . . . . . . . . . . 19 |- (E.t e. ~P1 ~P1 1c<<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.bE.t(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
37		snex 4111	. . . . . . . . . . . . . . . . . . . . . 22 |- {{{b}}} e. _V
38		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = {{{b}}} -> <<t, <<{y}, j>>>> = <<{{{b}}}, <<{y}, j>>>>)
39	38	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = {{{b}}} -> (<<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> <<{{{b}}}, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))))
40	37, 39	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> <<{{{b}}}, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
41		elin 3219	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{{b}}}, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (<<{{{b}}}, <<{y}, j>>>> e. Ins2k Sk /\ <<{{{b}}}, <<{y}, j>>>> e. (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
42		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {b} e. _V
43	42, 20, 2	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{b}}}, <<{y}, j>>>> e. Ins2k Sk <-> <<{b}, j>> e. Sk )
44		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . 24 |- b e. _V
45	44, 2	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{b}, j>> e. Sk <-> b e. j)
46	43, 45	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{{b}}}, <<{y}, j>>>> e. Ins2k Sk <-> b e. j)
47		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- <<{{{b}}}, <<{y}, j>>>> e. _V
48	47	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{b}}}, <<{y}, j>>>> e. (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
49		elpw141c 4150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.a t = {{{{{a}}}}})
50	49	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> (E.a t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
51		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.a(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> (E.a t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
52	50, 51	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.a(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
53	52	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.tE.a(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
54		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
55		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.tE.a(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
56	53, 54, 55	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
57		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {{{{{a}}}}} e. _V
58		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = {{{{{a}}}}} -> <<t, <<{{{b}}}, <<{y}, j>>>>>> = <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>)
59	58	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = {{{{{a}}}}} -> (<<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
60	57, 59	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
61		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
62		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- {{{a}}} e. _V
63	62, 37, 27	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins2k Sk <-> <<{{{a}}}, <<{y}, j>>>> e. Ins2k Sk )
64		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- {a} e. _V
65	64, 20, 2	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{a}}}, <<{y}, j>>>> e. Ins2k Sk <-> <<{a}, j>> e. Sk )
66		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- a e. _V
67	66, 2	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{a}, j>> e. Sk <-> a e. j)
68	63, 65, 67	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins2k Sk <-> a e. j)
69		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))
70	62, 37, 27	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{{a}}}, {{{b}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
71		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{a}} e. _V
72		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{b}} e. _V
73	71, 72	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{a}}}, {{{b}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{a}}, {{b}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
74	64, 42	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{a}}, {{b}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{a}, {b}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
75	66, 44	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{a}, {b}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<a, b>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
76	66, 44	ndisjrelk 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<a, b>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i b) =/= (/))
77	76	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (-. <<a, b>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. (a i^i b) =/= (/))
78		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- <<a, b>> e. _V
79	78	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<a, b>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. <<a, b>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
80		df-ne 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((a i^i b) =/= (/) <-> -. (a i^i b) = (/))
81	80	con2bii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((a i^i b) = (/) <-> -. (a i^i b) =/= (/))
82	77, 79, 81	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<a, b>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i b) = (/))
83	74, 75, 82	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{a}}, {{b}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i b) = (/))
84	70, 73, 83	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i b) = (/))
85		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. _V
86	85	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
87		elpw171c 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x t = {{{{{{{{x}}}}}}}})
88	87	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> (E.x t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
89		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (E.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> (E.x t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
90	88, 89	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
91	90	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.tE.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
92		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
93		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.tE.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
94	91, 92, 93	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
95		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {{{{{{{{x}}}}}}}} e. _V
96		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (t = {{{{{{{{x}}}}}}}} -> <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> = <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>>)
97	96	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (t = {{{{{{{{x}}}}}}}} -> (<<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
98	95, 97	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
99		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
100		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{{{{{x}}}}}} e. _V
101	100, 57, 47	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins3k SIk Sk )
102		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{{{x}}}} e. _V
103	102, 37, 27	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{x}}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{x}}}}, <<{y}, j>>>> e. Ins3k SIk Sk )
104		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {{x}} e. _V
105	104, 20, 2	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{x}}}}, <<{y}, j>>>> e. Ins3k SIk Sk <-> <<{{x}}, {y}>> e. SIk Sk )
106		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {x} e. _V
107	106, 23	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{x}}, {y}>> e. SIk Sk <-> <<{x}, y>> e. Sk )
108	21, 23	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{x}, y>> e. Sk <-> x e. y)
109	105, 107, 108	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{x}}}}, <<{y}, j>>>> e. Ins3k SIk Sk <-> x e. y)
110	101, 103, 109	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> x e. y)
111	100, 57, 47	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, {{{{{a}}}}}>> e. SIk SIk SIk SIk SIk Sk )
112		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {{{{{x}}}}} e. _V
113		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {{{{a}}}} e. _V
114	112, 113	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{{x}}}}}}, {{{{{a}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk )
115	102, 62	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{a}}}>> e. SIk SIk SIk Sk )
116		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- {{{x}}} e. _V
117	116, 71	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{{{x}}}}, {{{a}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{a}}>> e. SIk SIk Sk )
118	104, 64	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{{{x}}}, {{a}}>> e. SIk SIk Sk <-> <<{{x}}, {a}>> e. SIk Sk )
119	106, 66	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{{x}}, {a}>> e. SIk Sk <-> <<{x}, a>> e. Sk )
120	21, 66	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{x}, a>> e. Sk <-> x e. a)
121	118, 119, 120	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{{x}}}, {{a}}>> e. SIk SIk Sk <-> x e. a)
122	115, 117, 121	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk <-> x e. a)
123	111, 114, 122	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> x e. a)
124	100, 57, 47	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk Sk )
125	102, 37, 27	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{{x}}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk Sk )
126	116, 72	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{b}}>> e. SIk SIk Sk )
127	104, 42	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{{x}}}, {{b}}>> e. SIk SIk Sk <-> <<{{x}}, {b}>> e. SIk Sk )
128	106, 44	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{{x}}, {b}>> e. SIk Sk <-> <<{x}, b>> e. Sk )
129	21, 44	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{x}, b>> e. Sk <-> x e. b)
130	128, 129	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (<<{{x}}, {b}>> e. SIk Sk <-> x e. b)
131	126, 127, 130	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk Sk <-> x e. b)
132	124, 125, 131	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> x e. b)
133	123, 132	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ) <-> (x e. a \/ x e. b))
134		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ))
135		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x e. (a u. b) <-> (x e. a \/ x e. b))
136	133, 134, 135	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> x e. (a u. b))
137	110, 136	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> (x e. y <-> x e. (a u. b)))
138	137	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (-. (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (x e. y <-> x e. (a u. b)))
139	98, 99, 138	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> -. (x e. y <-> x e. (a u. b)))
140	139	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.x -. (x e. y <-> x e. (a u. b)))
141	86, 94, 140	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.x -. (x e. y <-> x e. (a u. b)))
142	141	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (-. <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. E.x -. (x e. y <-> x e. (a u. b)))
143	85	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))
144		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = (a u. b) <-> A.x(x e. y <-> x e. (a u. b)))
145		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.x(x e. y <-> x e. (a u. b)) <-> -. E.x -. (x e. y <-> x e. (a u. b)))
146	144, 145	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (a u. b) <-> -. E.x -. (x e. y <-> x e. (a u. b)))
147	142, 143, 146	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> y = (a u. b))
148	84, 147	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> ((a i^i b) = (/) /\ y = (a u. b)))
149	69, 148	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> ((a i^i b) = (/) /\ y = (a u. b)))
150	68, 149	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((<<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{a}}}}}, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> (a e. j /\ ((a i^i b) = (/) /\ y = (a u. b))))
151	60, 61, 150	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> (a e. j /\ ((a i^i b) = (/) /\ y = (a u. b))))
152	151	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{b}}}, <<{y}, j>>>>>> e. ( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.a(a e. j /\ ((a i^i b) = (/) /\ y = (a u. b))))
153	48, 56, 152	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{b}}}, <<{y}, j>>>> e. (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.a(a e. j /\ ((a i^i b) = (/) /\ y = (a u. b))))
154		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.a e. j ((a i^i b) = (/) /\ y = (a u. b)) <-> E.a(a e. j /\ ((a i^i b) = (/) /\ y = (a u. b))))
155	153, 154	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{{b}}}, <<{y}, j>>>> e. (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.a e. j ((a i^i b) = (/) /\ y = (a u. b)))
156	46, 155	anbi12i 678	. . . . . . . . . . . . . . . . . . . . 21 |- ((<<{{{b}}}, <<{y}, j>>>> e. Ins2k Sk /\ <<{{{b}}}, <<{y}, j>>>> e. (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (b e. j /\ E.a e. j ((a i^i b) = (/) /\ y = (a u. b))))
157	40, 41, 156	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> (b e. j /\ E.a e. j ((a i^i b) = (/) /\ y = (a u. b))))
158	157	exbii 1582	. . . . . . . . . . . . . . . . . . 19 |- (E.bE.t(t = {{{b}}} /\ <<t, <<{y}, j>>>> e. ( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))) <-> E.b(b e. j /\ E.a e. j ((a i^i b) = (/) /\ y = (a u. b))))
159	28, 36, 158	3bitri 262	. . . . . . . . . . . . . . . . . 18 |- (<<{y}, j>> e. (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.b(b e. j /\ E.a e. j ((a i^i b) = (/) /\ y = (a u. b))))
160		df-rex 2620	. . . . . . . . . . . . . . . . . 18 |- (E.b e. j E.a e. j ((a i^i b) = (/) /\ y = (a u. b)) <-> E.b(b e. j /\ E.a e. j ((a i^i b) = (/) /\ y = (a u. b))))
161	159, 160	bitr4i 243	. . . . . . . . . . . . . . . . 17 |- (<<{y}, j>> e. (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.b e. j E.a e. j ((a i^i b) = (/) /\ y = (a u. b)))
162		rexcom 2772	. . . . . . . . . . . . . . . . 17 |- (E.b e. j E.a e. j ((a i^i b) = (/) /\ y = (a u. b)) <-> E.a e. j E.b e. j ((a i^i b) = (/) /\ y = (a u. b)))
163	26, 161, 162	3bitri 262	. . . . . . . . . . . . . . . 16 |- (<<{{{y}}}, <<x, j>>>> e. Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.a e. j E.b e. j ((a i^i b) = (/) /\ y = (a u. b)))
164	25, 163	bibi12i 306	. . . . . . . . . . . . . . 15 |- ((<<{{{y}}}, <<x, j>>>> e. Ins3k Sk <-> <<{{{y}}}, <<x, j>>>> e. Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> (y e. x <-> E.a e. j E.b e. j ((a i^i b) = (/) /\ y = (a u. b))))
165	164	notbii 287	. . . . . . . . . . . . . 14 |- (-. (<<{{{y}}}, <<x, j>>>> e. Ins3k Sk <-> <<{{{y}}}, <<x, j>>>> e. Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> -. (y e. x <-> E.a e. j E.b e. j ((a i^i b) = (/) /\ y = (a u. b))))
166	18, 19, 165	3bitri 262	. . . . . . . . . . . . 13 |- (E.t(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> -. (y e. x <-> E.a e. j E.b e. j ((a i^i b) = (/) /\ y = (a u. b))))
167	166	exbii 1582	. . . . . . . . . . . 12 |- (E.yE.t(t = {{{y}}} /\ <<t, <<x, j>>>> e. ( Ins3k Sk (+) Ins2k (( Ins2k Sk i^i (( Ins2k Ins2k Sk i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))) <-> E.y