Theorem xpassen 6889

Description: Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)

Hypotheses

Ref	Expression
xpassen.1	|- A e. _V
xpassen.2	|- B e. _V
xpassen.3	|- C e. _V

Assertion

Ref	Expression
xpassen	|- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Proof of Theorem xpassen

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

Step	Hyp	Ref	Expression
1		xpassen.1	. . . 4 |- A e. _V
2		xpassen.2	. . . 4 |- B e. _V
3	1, 2	xpex 4778	. . 3 |- ( A X. B ) e. _V
4		xpassen.3	. . 3 |- C e. _V
5	3, 4	xpex 4778	. 2 |- ( ( A X. B ) X. C ) e. _V
6	2, 4	xpex 4778	. . 3 |- ( B X. C ) e. _V
7	1, 6	xpex 4778	. 2 |- ( A X. ( B X. C ) ) e. _V
8		vex 2766	. . . . . . . . . 10 |- x e. _V
9	8	snex 4218	. . . . . . . . 9 |- { x } e. _V
10	9	dmex 4932	. . . . . . . 8 |- dom { x } e. _V
11	10	uniex 4472	. . . . . . 7 |- U. dom { x } e. _V
12	11	snex 4218	. . . . . 6 |- { U. dom { x } } e. _V
13	12	dmex 4932	. . . . 5 |- dom { U. dom { x } } e. _V
14	13	uniex 4472	. . . 4 |- U. dom { U. dom { x } } e. _V
15	12	rnex 4933	. . . . . 6 |- ran { U. dom { x } } e. _V
16	15	uniex 4472	. . . . 5 |- U. ran { U. dom { x } } e. _V
17	9	rnex 4933	. . . . . 6 |- ran { x } e. _V
18	17	uniex 4472	. . . . 5 |- U. ran { x } e. _V
19	16, 18	opex 4262	. . . 4 |- <. U. ran { U. dom { x } } , U. ran { x } >. e. _V
20	14, 19	opex 4262	. . 3 |- <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. e. _V
21	20	a1i 9	. 2 |- ( x e. ( ( A X. B ) X. C ) -> <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. e. _V )
22		vex 2766	. . . . . . . 8 |- y e. _V
23	22	snex 4218	. . . . . . 7 |- { y } e. _V
24	23	dmex 4932	. . . . . 6 |- dom { y } e. _V
25	24	uniex 4472	. . . . 5 |- U. dom { y } e. _V
26	23	rnex 4933	. . . . . . . . 9 |- ran { y } e. _V
27	26	uniex 4472	. . . . . . . 8 |- U. ran { y } e. _V
28	27	snex 4218	. . . . . . 7 |- { U. ran { y } } e. _V
29	28	dmex 4932	. . . . . 6 |- dom { U. ran { y } } e. _V
30	29	uniex 4472	. . . . 5 |- U. dom { U. ran { y } } e. _V
31	25, 30	opex 4262	. . . 4 |- <. U. dom { y } , U. dom { U. ran { y } } >. e. _V
32	28	rnex 4933	. . . . 5 |- ran { U. ran { y } } e. _V
33	32	uniex 4472	. . . 4 |- U. ran { U. ran { y } } e. _V
34	31, 33	opex 4262	. . 3 |- <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. e. _V
35	34	a1i 9	. 2 |- ( y e. ( A X. ( B X. C ) ) -> <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. e. _V )
36		sneq 3633	. . . . . . . . . . . . . . . . 17 |- ( x = <. <. z , w >. , v >. -> { x } = { <. <. z , w >. , v >. } )
37	36	dmeqd 4868	. . . . . . . . . . . . . . . 16 |- ( x = <. <. z , w >. , v >. -> dom { x } = dom { <. <. z , w >. , v >. } )
38	37	unieqd 3850	. . . . . . . . . . . . . . 15 |- ( x = <. <. z , w >. , v >. -> U. dom { x } = U. dom { <. <. z , w >. , v >. } )
39	38	sneqd 3635	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> { U. dom { x } } = { U. dom { <. <. z , w >. , v >. } } )
40	39	dmeqd 4868	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> dom { U. dom { x } } = dom { U. dom { <. <. z , w >. , v >. } } )
41	40	unieqd 3850	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> U. dom { U. dom { x } } = U. dom { U. dom { <. <. z , w >. , v >. } } )
42		vex 2766	. . . . . . . . . . . . . . . . . 18 |- z e. _V
43		vex 2766	. . . . . . . . . . . . . . . . . 18 |- w e. _V
44	42, 43	opex 4262	. . . . . . . . . . . . . . . . 17 |- <. z , w >. e. _V
45		vex 2766	. . . . . . . . . . . . . . . . 17 |- v e. _V
46	44, 45	op1sta 5151	. . . . . . . . . . . . . . . 16 |- U. dom { <. <. z , w >. , v >. } = <. z , w >.
47	46	sneqi 3634	. . . . . . . . . . . . . . 15 |- { U. dom { <. <. z , w >. , v >. } } = { <. z , w >. }
48	47	dmeqi 4867	. . . . . . . . . . . . . 14 |- dom { U. dom { <. <. z , w >. , v >. } } = dom { <. z , w >. }
49	48	unieqi 3849	. . . . . . . . . . . . 13 |- U. dom { U. dom { <. <. z , w >. , v >. } } = U. dom { <. z , w >. }
50	42, 43	op1sta 5151	. . . . . . . . . . . . 13 |- U. dom { <. z , w >. } = z
51	49, 50	eqtri 2217	. . . . . . . . . . . 12 |- U. dom { U. dom { <. <. z , w >. , v >. } } = z
52	41, 51	eqtr2di 2246	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> z = U. dom { U. dom { x } } )
53	39	rneqd 4895	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { U. dom { x } } = ran { U. dom { <. <. z , w >. , v >. } } )
54	53	unieqd 3850	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { U. dom { x } } = U. ran { U. dom { <. <. z , w >. , v >. } } )
55	47	rneqi 4894	. . . . . . . . . . . . . . 15 |- ran { U. dom { <. <. z , w >. , v >. } } = ran { <. z , w >. }
56	55	unieqi 3849	. . . . . . . . . . . . . 14 |- U. ran { U. dom { <. <. z , w >. , v >. } } = U. ran { <. z , w >. }
57	42, 43	op2nda 5154	. . . . . . . . . . . . . 14 |- U. ran { <. z , w >. } = w
58	56, 57	eqtri 2217	. . . . . . . . . . . . 13 |- U. ran { U. dom { <. <. z , w >. , v >. } } = w
59	54, 58	eqtr2di 2246	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> w = U. ran { U. dom { x } } )
60	36	rneqd 4895	. . . . . . . . . . . . . 14 |- ( x = <. <. z , w >. , v >. -> ran { x } = ran { <. <. z , w >. , v >. } )
61	60	unieqd 3850	. . . . . . . . . . . . 13 |- ( x = <. <. z , w >. , v >. -> U. ran { x } = U. ran { <. <. z , w >. , v >. } )
62	44, 45	op2nda 5154	. . . . . . . . . . . . 13 |- U. ran { <. <. z , w >. , v >. } = v
63	61, 62	eqtr2di 2246	. . . . . . . . . . . 12 |- ( x = <. <. z , w >. , v >. -> v = U. ran { x } )
64	59, 63	opeq12d 3816	. . . . . . . . . . 11 |- ( x = <. <. z , w >. , v >. -> <. w , v >. = <. U. ran { U. dom { x } } , U. ran { x } >. )
65	52, 64	opeq12d 3816	. . . . . . . . . 10 |- ( x = <. <. z , w >. , v >. -> <. z , <. w , v >. >. = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. )
66		sneq 3633	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { y } = { <. z , <. w , v >. >. } )
67	66	dmeqd 4868	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { y } = dom { <. z , <. w , v >. >. } )
68	67	unieqd 3850	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { y } = U. dom { <. z , <. w , v >. >. } )
69	43, 45	opex 4262	. . . . . . . . . . . . . 14 |- <. w , v >. e. _V
70	42, 69	op1sta 5151	. . . . . . . . . . . . 13 |- U. dom { <. z , <. w , v >. >. } = z
71	68, 70	eqtr2di 2246	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> z = U. dom { y } )
72	66	rneqd 4895	. . . . . . . . . . . . . . . . 17 |- ( y = <. z , <. w , v >. >. -> ran { y } = ran { <. z , <. w , v >. >. } )
73	72	unieqd 3850	. . . . . . . . . . . . . . . 16 |- ( y = <. z , <. w , v >. >. -> U. ran { y } = U. ran { <. z , <. w , v >. >. } )
74	73	sneqd 3635	. . . . . . . . . . . . . . 15 |- ( y = <. z , <. w , v >. >. -> { U. ran { y } } = { U. ran { <. z , <. w , v >. >. } } )
75	74	dmeqd 4868	. . . . . . . . . . . . . 14 |- ( y = <. z , <. w , v >. >. -> dom { U. ran { y } } = dom { U. ran { <. z , <. w , v >. >. } } )
76	75	unieqd 3850	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> U. dom { U. ran { y } } = U. dom { U. ran { <. z , <. w , v >. >. } } )
77	42, 69	op2nda 5154	. . . . . . . . . . . . . . . . 17 |- U. ran { <. z , <. w , v >. >. } = <. w , v >.
78	77	sneqi 3634	. . . . . . . . . . . . . . . 16 |- { U. ran { <. z , <. w , v >. >. } } = { <. w , v >. }
79	78	dmeqi 4867	. . . . . . . . . . . . . . 15 |- dom { U. ran { <. z , <. w , v >. >. } } = dom { <. w , v >. }
80	79	unieqi 3849	. . . . . . . . . . . . . 14 |- U. dom { U. ran { <. z , <. w , v >. >. } } = U. dom { <. w , v >. }
81	43, 45	op1sta 5151	. . . . . . . . . . . . . 14 |- U. dom { <. w , v >. } = w
82	80, 81	eqtri 2217	. . . . . . . . . . . . 13 |- U. dom { U. ran { <. z , <. w , v >. >. } } = w
83	76, 82	eqtr2di 2246	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> w = U. dom { U. ran { y } } )
84	71, 83	opeq12d 3816	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> <. z , w >. = <. U. dom { y } , U. dom { U. ran { y } } >. )
85	74	rneqd 4895	. . . . . . . . . . . . 13 |- ( y = <. z , <. w , v >. >. -> ran { U. ran { y } } = ran { U. ran { <. z , <. w , v >. >. } } )
86	85	unieqd 3850	. . . . . . . . . . . 12 |- ( y = <. z , <. w , v >. >. -> U. ran { U. ran { y } } = U. ran { U. ran { <. z , <. w , v >. >. } } )
87	78	rneqi 4894	. . . . . . . . . . . . . 14 |- ran { U. ran { <. z , <. w , v >. >. } } = ran { <. w , v >. }
88	87	unieqi 3849	. . . . . . . . . . . . 13 |- U. ran { U. ran { <. z , <. w , v >. >. } } = U. ran { <. w , v >. }
89	43, 45	op2nda 5154	. . . . . . . . . . . . 13 |- U. ran { <. w , v >. } = v
90	88, 89	eqtri 2217	. . . . . . . . . . . 12 |- U. ran { U. ran { <. z , <. w , v >. >. } } = v
91	86, 90	eqtr2di 2246	. . . . . . . . . . 11 |- ( y = <. z , <. w , v >. >. -> v = U. ran { U. ran { y } } )
92	84, 91	opeq12d 3816	. . . . . . . . . 10 |- ( y = <. z , <. w , v >. >. -> <. <. z , w >. , v >. = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. )
93	65, 92	eq2tri 2256	. . . . . . . . 9 |- ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
94		anass 401	. . . . . . . . 9 |- ( ( ( z e. A /\ w e. B ) /\ v e. C ) <-> ( z e. A /\ ( w e. B /\ v e. C ) ) )
95	93, 94	anbi12i 460	. . . . . . . 8 |- ( ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) <-> ( ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
96		an32 562	. . . . . . . 8 |- ( ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( ( x = <. <. z , w >. , v >. /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
97		an32 562	. . . . . . . 8 |- ( ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( ( y = <. z , <. w , v >. >. /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
98	95, 96, 97	3bitr4i 212	. . . . . . 7 |- ( ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
99	98	exbii 1619	. . . . . 6 |- ( E. v ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> E. v ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
100		19.41v 1917	. . . . . 6 |- ( E. v ( ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
101		19.41v 1917	. . . . . 6 |- ( E. v ( ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
102	99, 100, 101	3bitr3i 210	. . . . 5 |- ( ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
103	102	2exbii 1620	. . . 4 |- ( E. z E. w ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> E. z E. w ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
104		19.41vv 1918	. . . 4 |- ( E. z E. w ( E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
105		19.41vv 1918	. . . 4 |- ( E. z E. w ( E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
106	103, 104, 105	3bitr3i 210	. . 3 |- ( ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
107		elxp 4680	. . . . 5 |- ( x e. ( ( A X. B ) X. C ) <-> E. u E. v ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) )
108		excom 1678	. . . . 5 |- ( E. u E. v ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) )
109		elxp 4680	. . . . . . . . 9 |- ( u e. ( A X. B ) <-> E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) )
110	109	anbi1i 458	. . . . . . . 8 |- ( ( u e. ( A X. B ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
111		an12 561	. . . . . . . 8 |- ( ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> ( u e. ( A X. B ) /\ ( x = <. u , v >. /\ v e. C ) ) )
112		19.41vv 1918	. . . . . . . 8 |- ( E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( E. z E. w ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
113	110, 111, 112	3bitr4i 212	. . . . . . 7 |- ( ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
114	113	2exbii 1620	. . . . . 6 |- ( E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. v E. u E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
115		exrot4 1705	. . . . . 6 |- ( E. v E. u E. z E. w ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. z E. w E. v E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) )
116		anass 401	. . . . . . . . 9 |- ( ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) )
117	116	exbii 1619	. . . . . . . 8 |- ( E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. u ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) )
118		opeq1 3808	. . . . . . . . . . . 12 |- ( u = <. z , w >. -> <. u , v >. = <. <. z , w >. , v >. )
119	118	eqeq2d 2208	. . . . . . . . . . 11 |- ( u = <. z , w >. -> ( x = <. u , v >. <-> x = <. <. z , w >. , v >. ) )
120	119	anbi1d 465	. . . . . . . . . 10 |- ( u = <. z , w >. -> ( ( x = <. u , v >. /\ v e. C ) <-> ( x = <. <. z , w >. , v >. /\ v e. C ) ) )
121	120	anbi2d 464	. . . . . . . . 9 |- ( u = <. z , w >. -> ( ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) ) )
122	44, 121	ceqsexv 2802	. . . . . . . 8 |- ( E. u ( u = <. z , w >. /\ ( ( z e. A /\ w e. B ) /\ ( x = <. u , v >. /\ v e. C ) ) ) <-> ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) )
123		an12 561	. . . . . . . 8 |- ( ( ( z e. A /\ w e. B ) /\ ( x = <. <. z , w >. , v >. /\ v e. C ) ) <-> ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
124	117, 122, 123	3bitri 206	. . . . . . 7 |- ( E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
125	124	3exbii 1621	. . . . . 6 |- ( E. z E. w E. v E. u ( ( u = <. z , w >. /\ ( z e. A /\ w e. B ) ) /\ ( x = <. u , v >. /\ v e. C ) ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
126	114, 115, 125	3bitri 206	. . . . 5 |- ( E. v E. u ( x = <. u , v >. /\ ( u e. ( A X. B ) /\ v e. C ) ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
127	107, 108, 126	3bitri 206	. . . 4 |- ( x e. ( ( A X. B ) X. C ) <-> E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) )
128	127	anbi1i 458	. . 3 |- ( ( x e. ( ( A X. B ) X. C ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( E. z E. w E. v ( x = <. <. z , w >. , v >. /\ ( ( z e. A /\ w e. B ) /\ v e. C ) ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) )
129		elxp 4680	. . . . 5 |- ( y e. ( A X. ( B X. C ) ) <-> E. z E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) )
130		elxp 4680	. . . . . . . . . 10 |- ( u e. ( B X. C ) <-> E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) )
131	130	anbi2i 457	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ u e. ( B X. C ) ) <-> ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) )
132		anass 401	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ u e. ( B X. C ) ) <-> ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) )
133		19.42vv 1926	. . . . . . . . . 10 |- ( E. w E. v ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) )
134		an12 561	. . . . . . . . . . . 12 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) ) )
135		anass 401	. . . . . . . . . . . . 13 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) <-> ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
136	135	anbi2i 457	. . . . . . . . . . . 12 |- ( ( u = <. w , v >. /\ ( ( y = <. z , u >. /\ z e. A ) /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
137	134, 136	bitri 184	. . . . . . . . . . 11 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
138	137	2exbii 1620	. . . . . . . . . 10 |- ( E. w E. v ( ( y = <. z , u >. /\ z e. A ) /\ ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
139	133, 138	bitr3i 186	. . . . . . . . 9 |- ( ( ( y = <. z , u >. /\ z e. A ) /\ E. w E. v ( u = <. w , v >. /\ ( w e. B /\ v e. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
140	131, 132, 139	3bitr3i 210	. . . . . . . 8 |- ( ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
141	140	exbii 1619	. . . . . . 7 |- ( E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. u E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
142		exrot3 1704	. . . . . . 7 |- ( E. u E. w E. v ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> E. w E. v E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
143		opeq2 3809	. . . . . . . . . . 11 |- ( u = <. w , v >. -> <. z , u >. = <. z , <. w , v >. >. )
144	143	eqeq2d 2208	. . . . . . . . . 10 |- ( u = <. w , v >. -> ( y = <. z , u >. <-> y = <. z , <. w , v >. >. ) )
145	144	anbi1d 465	. . . . . . . . 9 |- ( u = <. w , v >. -> ( ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) <-> ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) )
146	69, 145	ceqsexv 2802	. . . . . . . 8 |- ( E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
147	146	2exbii 1620	. . . . . . 7 |- ( E. w E. v E. u ( u = <. w , v >. /\ ( y = <. z , u >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) ) <-> E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
148	141, 142, 147	3bitri 206	. . . . . 6 |- ( E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
149	148	exbii 1619	. . . . 5 |- ( E. z E. u ( y = <. z , u >. /\ ( z e. A /\ u e. ( B X. C ) ) ) <-> E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
150	129, 149	bitri 184	. . . 4 |- ( y e. ( A X. ( B X. C ) ) <-> E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) )
151	150	anbi1i 458	. . 3 |- ( ( y e. ( A X. ( B X. C ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) <-> ( E. z E. w E. v ( y = <. z , <. w , v >. >. /\ ( z e. A /\ ( w e. B /\ v e. C ) ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
152	106, 128, 151	3bitr4i 212	. 2 |- ( ( x e. ( ( A X. B ) X. C ) /\ y = <. U. dom { U. dom { x } } , <. U. ran { U. dom { x } } , U. ran { x } >. >. ) <-> ( y e. ( A X. ( B X. C ) ) /\ x = <. <. U. dom { y } , U. dom { U. ran { y } } >. , U. ran { U. ran { y } } >. ) )
153	5, 7, 21, 35, 152	en2i 6829	1 |- ( ( A X. B ) X. C ) ~~ ( A X. ( B X. C ) )

Syntax hints:   /\ wa 104   = wceq 1364   E.wex 1506   e. wcel 2167   _Vcvv 2763   {csn 3622   <.cop 3625   U.cuni 3839   class class class wbr 4033   X. cxp 4661   dom cdm 4663   ran crn 4664   ~~ cen 6797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-en 6800

This theorem is referenced by: (None)