Theorem xpassen 6240

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 4396	. . 3 |- (A X. B) e. _V
4		xpassen.3	. . 3 |- C e. _V
5	3, 4	xpex 4396	. 2 |- ((A X. B) X. C) e. _V
6	2, 4	xpex 4396	. . 3 |- (B X. C) e. _V
7	1, 6	xpex 4396	. 2 |- (A X. (B X. C)) e. _V
8		vex 2554	. . . . . . . . . 10 |- x e. _V
9	8	snex 3928	. . . . . . . . 9 |- {x } e. _V
10	9	dmex 4541	. . . . . . . 8 |- dom {x } e. _V
11	10	uniex 4140	. . . . . . 7 |- U. dom {x } e. _V
12	11	snex 3928	. . . . . 6 |- { U. dom {x } } e. _V
13	12	dmex 4541	. . . . 5 |- dom { U. dom {x } } e. _V
14	13	uniex 4140	. . . 4 |- U. dom { U. dom {x } } e. _V
15	12	rnex 4542	. . . . . 6 |- ran { U. dom {x } } e. _V
16	15	uniex 4140	. . . . 5 |- U. ran { U. dom {x } } e. _V
17	9	rnex 4542	. . . . . 6 |- ran {x } e. _V
18	17	uniex 4140	. . . . 5 |- U. ran {x } e. _V
19	16, 18	opex 3957	. . . 4 |- <. U. ran { U. dom {x } } , U. ran {x } >. e. _V
20	14, 19	opex 3957	. . 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 2554	. . . . . . . 8 |- y e. _V
23	22	snex 3928	. . . . . . 7 |- {y } e. _V
24	23	dmex 4541	. . . . . 6 |- dom {y } e. _V
25	24	uniex 4140	. . . . 5 |- U. dom {y } e. _V
26	23	rnex 4542	. . . . . . . . 9 |- ran {y } e. _V
27	26	uniex 4140	. . . . . . . 8 |- U. ran {y } e. _V
28	27	snex 3928	. . . . . . 7 |- { U. ran {y } } e. _V
29	28	dmex 4541	. . . . . 6 |- dom { U. ran {y } } e. _V
30	29	uniex 4140	. . . . 5 |- U. dom { U. ran {y } } e. _V
31	25, 30	opex 3957	. . . 4 |- <. U. dom {y } , U. dom { U. ran {y } } >. e. _V
32	28	rnex 4542	. . . . 5 |- ran { U. ran {y } } e. _V
33	32	uniex 4140	. . . 4 |- U. ran { U. ran {y } } e. _V
34	31, 33	opex 3957	. . 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 3378	. . . . . . . . . . . . . . . . 17 |- (x = <. <.z , w >. , v >. -> {x } = { <. <.z , w >. , v >. })
37	36	dmeqd 4480	. . . . . . . . . . . . . . . 16 |- (x = <. <.z , w >. , v >. -> dom {x } = dom { <. <.z , w >. , v >. })
38	37	unieqd 3582	. . . . . . . . . . . . . . 15 |- (x = <. <.z , w >. , v >. -> U. dom {x } = U. dom { <. <.z , w >. , v >. })
39	38	sneqd 3380	. . . . . . . . . . . . . 14 |- (x = <. <.z , w >. , v >. -> { U. dom {x } } = { U. dom { <. <.z , w >. , v >. } })
40	39	dmeqd 4480	. . . . . . . . . . . . 13 |- (x = <. <.z , w >. , v >. -> dom { U. dom {x } } = dom { U. dom { <. <.z , w >. , v >. } })
41	40	unieqd 3582	. . . . . . . . . . . 12 |- (x = <. <.z , w >. , v >. -> U. dom { U. dom {x } } = U. dom { U. dom { <. <.z , w >. , v >. } })
42		vex 2554	. . . . . . . . . . . . . . . . . 18 |- z e. _V
43		vex 2554	. . . . . . . . . . . . . . . . . 18 |- w e. _V
44	42, 43	opex 3957	. . . . . . . . . . . . . . . . 17 |- <.z , w >. e. _V
45		vex 2554	. . . . . . . . . . . . . . . . 17 |- v e. _V
46	44, 45	op1sta 4745	. . . . . . . . . . . . . . . 16 |- U. dom { <. <.z , w >. , v >. } = <.z , w >.
47	46	sneqi 3379	. . . . . . . . . . . . . . 15 |- { U. dom { <. <.z , w >. , v >. } } = { <.z , w >. }
48	47	dmeqi 4479	. . . . . . . . . . . . . 14 |- dom { U. dom { <. <.z , w >. , v >. } } = dom { <.z , w >. }
49	48	unieqi 3581	. . . . . . . . . . . . 13 |- U. dom { U. dom { <. <.z , w >. , v >. } } = U. dom { <.z , w >. }
50	42, 43	op1sta 4745	. . . . . . . . . . . . 13 |- U. dom { <.z , w >. } = z
51	49, 50	eqtri 2057	. . . . . . . . . . . 12 |- U. dom { U. dom { <. <.z , w >. , v >. } } = z
52	41, 51	syl6req 2086	. . . . . . . . . . 11 |- (x = <. <.z , w >. , v >. -> z = U. dom { U. dom {x } })
53	39	rneqd 4506	. . . . . . . . . . . . . 14 |- (x = <. <.z , w >. , v >. -> ran { U. dom {x } } = ran { U. dom { <. <.z , w >. , v >. } })
54	53	unieqd 3582	. . . . . . . . . . . . 13 |- (x = <. <.z , w >. , v >. -> U. ran { U. dom {x } } = U. ran { U. dom { <. <.z , w >. , v >. } })
55	47	rneqi 4505	. . . . . . . . . . . . . . 15 |- ran { U. dom { <. <.z , w >. , v >. } } = ran { <.z , w >. }
56	55	unieqi 3581	. . . . . . . . . . . . . 14 |- U. ran { U. dom { <. <.z , w >. , v >. } } = U. ran { <.z , w >. }
57	42, 43	op2nda 4748	. . . . . . . . . . . . . 14 |- U. ran { <.z , w >. } = w
58	56, 57	eqtri 2057	. . . . . . . . . . . . 13 |- U. ran { U. dom { <. <.z , w >. , v >. } } = w
59	54, 58	syl6req 2086	. . . . . . . . . . . 12 |- (x = <. <.z , w >. , v >. -> w = U. ran { U. dom {x } })
60	36	rneqd 4506	. . . . . . . . . . . . . 14 |- (x = <. <.z , w >. , v >. -> ran {x } = ran { <. <.z , w >. , v >. })
61	60	unieqd 3582	. . . . . . . . . . . . 13 |- (x = <. <.z , w >. , v >. -> U. ran {x } = U. ran { <. <.z , w >. , v >. })
62	44, 45	op2nda 4748	. . . . . . . . . . . . 13 |- U. ran { <. <.z , w >. , v >. } = v
63	61, 62	syl6req 2086	. . . . . . . . . . . 12 |- (x = <. <.z , w >. , v >. -> v = U. ran {x })
64	59, 63	opeq12d 3548	. . . . . . . . . . 11 |- (x = <. <.z , w >. , v >. -> <.w , v >. = <. U. ran { U. dom {x } } , U. ran {x } >.)
65	52, 64	opeq12d 3548	. . . . . . . . . 10 |- (x = <. <.z , w >. , v >. -> <.z , <.w , v >. >. = <. U. dom { U. dom {x } } , <. U. ran { U. dom {x } } , U. ran {x } >. >.)
66		sneq 3378	. . . . . . . . . . . . . . 15 |- (y = <.z , <.w , v >. >. -> {y } = { <.z , <.w , v >. >. })
67	66	dmeqd 4480	. . . . . . . . . . . . . 14 |- (y = <.z , <.w , v >. >. -> dom {y } = dom { <.z , <.w , v >. >. })
68	67	unieqd 3582	. . . . . . . . . . . . 13 |- (y = <.z , <.w , v >. >. -> U. dom {y } = U. dom { <.z , <.w , v >. >. })
69	43, 45	opex 3957	. . . . . . . . . . . . . 14 |- <.w , v >. e. _V
70	42, 69	op1sta 4745	. . . . . . . . . . . . 13 |- U. dom { <.z , <.w , v >. >. } = z
71	68, 70	syl6req 2086	. . . . . . . . . . . 12 |- (y = <.z , <.w , v >. >. -> z = U. dom {y })
72	66	rneqd 4506	. . . . . . . . . . . . . . . . 17 |- (y = <.z , <.w , v >. >. -> ran {y } = ran { <.z , <.w , v >. >. })
73	72	unieqd 3582	. . . . . . . . . . . . . . . 16 |- (y = <.z , <.w , v >. >. -> U. ran {y } = U. ran { <.z , <.w , v >. >. })
74	73	sneqd 3380	. . . . . . . . . . . . . . 15 |- (y = <.z , <.w , v >. >. -> { U. ran {y } } = { U. ran { <.z , <.w , v >. >. } })
75	74	dmeqd 4480	. . . . . . . . . . . . . 14 |- (y = <.z , <.w , v >. >. -> dom { U. ran {y } } = dom { U. ran { <.z , <.w , v >. >. } })
76	75	unieqd 3582	. . . . . . . . . . . . 13 |- (y = <.z , <.w , v >. >. -> U. dom { U. ran {y } } = U. dom { U. ran { <.z , <.w , v >. >. } })
77	42, 69	op2nda 4748	. . . . . . . . . . . . . . . . 17 |- U. ran { <.z , <.w , v >. >. } = <.w , v >.
78	77	sneqi 3379	. . . . . . . . . . . . . . . 16 |- { U. ran { <.z , <.w , v >. >. } } = { <.w , v >. }
79	78	dmeqi 4479	. . . . . . . . . . . . . . 15 |- dom { U. ran { <.z , <.w , v >. >. } } = dom { <.w , v >. }
80	79	unieqi 3581	. . . . . . . . . . . . . 14 |- U. dom { U. ran { <.z , <.w , v >. >. } } = U. dom { <.w , v >. }
81	43, 45	op1sta 4745	. . . . . . . . . . . . . 14 |- U. dom { <.w , v >. } = w
82	80, 81	eqtri 2057	. . . . . . . . . . . . 13 |- U. dom { U. ran { <.z , <.w , v >. >. } } = w
83	76, 82	syl6req 2086	. . . . . . . . . . . 12 |- (y = <.z , <.w , v >. >. -> w = U. dom { U. ran {y } })
84	71, 83	opeq12d 3548	. . . . . . . . . . 11 |- (y = <.z , <.w , v >. >. -> <.z , w >. = <. U. dom {y } , U. dom { U. ran {y } } >.)
85	74	rneqd 4506	. . . . . . . . . . . . 13 |- (y = <.z , <.w , v >. >. -> ran { U. ran {y } } = ran { U. ran { <.z , <.w , v >. >. } })
86	85	unieqd 3582	. . . . . . . . . . . 12 |- (y = <.z , <.w , v >. >. -> U. ran { U. ran {y } } = U. ran { U. ran { <.z , <.w , v >. >. } })
87	78	rneqi 4505	. . . . . . . . . . . . . 14 |- ran { U. ran { <.z , <.w , v >. >. } } = ran { <.w , v >. }
88	87	unieqi 3581	. . . . . . . . . . . . 13 |- U. ran { U. ran { <.z , <.w , v >. >. } } = U. ran { <.w , v >. }
89	43, 45	op2nda 4748	. . . . . . . . . . . . 13 |- U. ran { <.w , v >. } = v
90	88, 89	eqtri 2057	. . . . . . . . . . . 12 |- U. ran { U. ran { <.z , <.w , v >. >. } } = v
91	86, 90	syl6req 2086	. . . . . . . . . . 11 |- (y = <.z , <.w , v >. >. -> v = U. ran { U. ran {y } })
92	84, 91	opeq12d 3548	. . . . . . . . . 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 2096	. . . . . . . . 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 381	. . . . . . . . 9 |- (((z e. A /\ w e. B) /\ v e. C) <-> (z e. A /\ (w e. B /\ v e. C)))
95	93, 94	anbi12i 433	. . . . . . . 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 496	. . . . . . . 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 496	. . . . . . . 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 201	. . . . . . 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 1493	. . . . . 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 1779	. . . . . 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 1779	. . . . . 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 199	. . . . 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 1494	. . . 4 |- (E.zE.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.zE.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 1780	. . . 4 |- (E.zE.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.zE.wE.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 1780	. . . 4 |- (E.zE.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.zE.wE.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 199	. . 3 |- ((E.zE.wE.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.zE.wE.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 4305	. . . . 5 |- (x e. ((A X. B) X. C) <-> E.uE.v(x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)))
108		excom 1551	. . . . 5 |- (E.uE.v(x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)) <-> E.vE.u(x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)))
109		elxp 4305	. . . . . . . . 9 |- (u e. (A X. B) <-> E.zE.w(u = <.z , w >. /\ (z e. A /\ w e. B)))
110	109	anbi1i 431	. . . . . . . 8 |- ((u e. (A X. B) /\ (x = <.u , v >. /\ v e. C)) <-> (E.zE.w(u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)))
111		an12 495	. . . . . . . 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 1780	. . . . . . . 8 |- (E.zE.w((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)) <-> (E.zE.w(u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)))
113	110, 111, 112	3bitr4i 201	. . . . . . 7 |- ((x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)) <-> E.zE.w((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)))
114	113	2exbii 1494	. . . . . 6 |- (E.vE.u(x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)) <-> E.vE.uE.zE.w((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)))
115		exrot4 1578	. . . . . 6 |- (E.vE.uE.zE.w((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)) <-> E.zE.wE.vE.u((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)))
116		anass 381	. . . . . . . . 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 1493	. . . . . . . 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 3540	. . . . . . . . . . . 12 |- (u = <.z , w >. -> <.u , v >. = <. <.z , w >. , v >.)
119	118	eqeq2d 2048	. . . . . . . . . . 11 |- (u = <.z , w >. -> (x = <.u , v >. <-> x = <. <.z , w >. , v >.))
120	119	anbi1d 438	. . . . . . . . . 10 |- (u = <.z , w >. -> ((x = <.u , v >. /\ v e. C) <-> (x = <. <.z , w >. , v >. /\ v e. C)))
121	120	anbi2d 437	. . . . . . . . 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 2587	. . . . . . . 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 495	. . . . . . . 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 195	. . . . . . 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 1495	. . . . . 6 |- (E.zE.wE.vE.u((u = <.z , w >. /\ (z e. A /\ w e. B)) /\ (x = <.u , v >. /\ v e. C)) <-> E.zE.wE.v(x = <. <.z , w >. , v >. /\ ((z e. A /\ w e. B) /\ v e. C)))
126	114, 115, 125	3bitri 195	. . . . 5 |- (E.vE.u(x = <.u , v >. /\ (u e. (A X. B) /\ v e. C)) <-> E.zE.wE.v(x = <. <.z , w >. , v >. /\ ((z e. A /\ w e. B) /\ v e. C)))
127	107, 108, 126	3bitri 195	. . . 4 |- (x e. ((A X. B) X. C) <-> E.zE.wE.v(x = <. <.z , w >. , v >. /\ ((z e. A /\ w e. B) /\ v e. C)))
128	127	anbi1i 431	. . 3 |- ((x e. ((A X. B) X. C) /\ y = <. U. dom { U. dom {x } } , <. U. ran { U. dom {x } } , U. ran {x } >. >.) <-> (E.zE.wE.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 4305	. . . . 5 |- (y e. (A X. (B X. C)) <-> E.zE.u(y = <.z , u >. /\ (z e. A /\ u e. (B X. C))))
130		elxp 4305	. . . . . . . . . 10 |- (u e. (B X. C) <-> E.wE.v(u = <.w , v >. /\ (w e. B /\ v e. C)))
131	130	anbi2i 430	. . . . . . . . 9 |- (((y = <.z , u >. /\ z e. A) /\ u e. (B X. C)) <-> ((y = <.z , u >. /\ z e. A) /\ E.wE.v(u = <.w , v >. /\ (w e. B /\ v e. C))))
132		anass 381	. . . . . . . . 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 1785	. . . . . . . . . 10 |- (E.wE.v((y = <.z , u >. /\ z e. A) /\ (u = <.w , v >. /\ (w e. B /\ v e. C))) <-> ((y = <.z , u >. /\ z e. A) /\ E.wE.v(u = <.w , v >. /\ (w e. B /\ v e. C))))
134		an12 495	. . . . . . . . . . . 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 381	. . . . . . . . . . . . 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 430	. . . . . . . . . . . 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 173	. . . . . . . . . . 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 1494	. . . . . . . . . 10 |- (E.wE.v((y = <.z , u >. /\ z e. A) /\ (u = <.w , v >. /\ (w e. B /\ v e. C))) <-> E.wE.v(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))))
139	133, 138	bitr3i 175	. . . . . . . . 9 |- (((y = <.z , u >. /\ z e. A) /\ E.wE.v(u = <.w , v >. /\ (w e. B /\ v e. C))) <-> E.wE.v(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))))
140	131, 132, 139	3bitr3i 199	. . . . . . . 8 |- ((y = <.z , u >. /\ (z e. A /\ u e. (B X. C))) <-> E.wE.v(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))))
141	140	exbii 1493	. . . . . . 7 |- (E.u(y = <.z , u >. /\ (z e. A /\ u e. (B X. C))) <-> E.uE.wE.v(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))))
142		exrot3 1577	. . . . . . 7 |- (E.uE.wE.v(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))) <-> E.wE.vE.u(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))))
143		opeq2 3541	. . . . . . . . . . 11 |- (u = <.w , v >. -> <.z , u >. = <.z , <.w , v >. >.)
144	143	eqeq2d 2048	. . . . . . . . . 10 |- (u = <.w , v >. -> (y = <.z , u >. <-> y = <.z , <.w , v >. >.))
145	144	anbi1d 438	. . . . . . . . 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 2587	. . . . . . . 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 1494	. . . . . . 7 |- (E.wE.vE.u(u = <.w , v >. /\ (y = <.z , u >. /\ (z e. A /\ (w e. B /\ v e. C)))) <-> E.wE.v(y = <.z , <.w , v >. >. /\ (z e. A /\ (w e. B /\ v e. C))))
148	141, 142, 147	3bitri 195	. . . . . 6 |- (E.u(y = <.z , u >. /\ (z e. A /\ u e. (B X. C))) <-> E.wE.v(y = <.z , <.w , v >. >. /\ (z e. A /\ (w e. B /\ v e. C))))
149	148	exbii 1493	. . . . 5 |- (E.zE.u(y = <.z , u >. /\ (z e. A /\ u e. (B X. C))) <-> E.zE.wE.v(y = <.z , <.w , v >. >. /\ (z e. A /\ (w e. B /\ v e. C))))
150	129, 149	bitri 173	. . . 4 |- (y e. (A X. (B X. C)) <-> E.zE.wE.v(y = <.z , <.w , v >. >. /\ (z e. A /\ (w e. B /\ v e. C))))
151	150	anbi1i 431	. . 3 |- ((y e. (A X. (B X. C)) /\ x = <. <. U. dom {y } , U. dom { U. ran {y } } >. , U. ran { U. ran {y } } >.) <-> (E.zE.wE.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 201	. 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 6186	1 |- ((A X. B) X. C) ~~ (A X. (B X. C))

Syntax hints:   /\ wa 97   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   {csn 3367   <.cop 3370   U.cuni 3571   class class class wbr 3755   X. cxp 4286   dom cdm 4288   ran crn 4289   ~~ cen 6155

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-en 6158

This theorem is referenced by: (None)