NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  xpassen GIF version

Theorem xpassen 6057
Description: Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by SF, 24-Feb-2015.)
Hypotheses
Ref Expression
xpassen.1 A V
xpassen.2 B V
xpassen.3 C V
Assertion
Ref Expression
xpassen ((A × B) × C) ≈ (A × (B × C))

Proof of Theorem xpassen
Dummy variables a b c x y z t p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stfo 5505 . . . . . . . . . . 11 1st :V–onto→V
2 fof 5269 . . . . . . . . . . 11 (1st :V–onto→V → 1st :V–→V)
31, 2ax-mp 5 . . . . . . . . . 10 1st :V–→V
4 dffn2 5224 . . . . . . . . . 10 (1st Fn V ↔ 1st :V–→V)
53, 4mpbir 200 . . . . . . . . 9 1st Fn V
6 ssv 3291 . . . . . . . . 9 ran 1st V
7 fnco 5191 . . . . . . . . 9 ((1st Fn V 1st Fn V ran 1st V) → (1st 1st ) Fn V)
85, 5, 6, 7mp3an 1277 . . . . . . . 8 (1st 1st ) Fn V
9 2ndfo 5506 . . . . . . . . . . . 12 2nd :V–onto→V
10 fofn 5271 . . . . . . . . . . . 12 (2nd :V–onto→V → 2nd Fn V)
119, 10ax-mp 5 . . . . . . . . . . 11 2nd Fn V
12 fnco 5191 . . . . . . . . . . 11 ((2nd Fn V 1st Fn V ran 1st V) → (2nd 1st ) Fn V)
1311, 5, 6, 12mp3an 1277 . . . . . . . . . 10 (2nd 1st ) Fn V
14 fntxp 5804 . . . . . . . . . 10 (((2nd 1st ) Fn V 2nd Fn V) → ((2nd 1st ) ⊗ 2nd ) Fn (V ∩ V))
1513, 11, 14mp2an 653 . . . . . . . . 9 ((2nd 1st ) ⊗ 2nd ) Fn (V ∩ V)
16 inidm 3464 . . . . . . . . . 10 (V ∩ V) = V
1716fneq2i 5179 . . . . . . . . 9 (((2nd 1st ) ⊗ 2nd ) Fn (V ∩ V) ↔ ((2nd 1st ) ⊗ 2nd ) Fn V)
1815, 17mpbi 199 . . . . . . . 8 ((2nd 1st ) ⊗ 2nd ) Fn V
19 fntxp 5804 . . . . . . . 8 (((1st 1st ) Fn V ((2nd 1st ) ⊗ 2nd ) Fn V) → ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn (V ∩ V))
208, 18, 19mp2an 653 . . . . . . 7 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn (V ∩ V)
2116fneq2i 5179 . . . . . . 7 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn (V ∩ V) ↔ ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn V)
2220, 21mpbi 199 . . . . . 6 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn V
23 dffn2 5224 . . . . . 6 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) Fn V ↔ ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–→V)
2422, 23mpbi 199 . . . . 5 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–→V
25 xpassenlem 6056 . . . . . . . . 9 (y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x ↔ ( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x))
26 xpassenlem 6056 . . . . . . . . 9 (z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x ↔ ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x))
27 simp1 955 . . . . . . . . . . . . . 14 (( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) → Proj1 Proj1 y = Proj1 x)
28 simp1 955 . . . . . . . . . . . . . 14 (( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x) → Proj1 Proj1 z = Proj1 x)
29 eqtr3 2372 . . . . . . . . . . . . . 14 (( Proj1 Proj1 y = Proj1 x Proj1 Proj1 z = Proj1 x) → Proj1 Proj1 y = Proj1 Proj1 z)
3027, 28, 29syl2an 463 . . . . . . . . . . . . 13 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj1 Proj1 y = Proj1 Proj1 z)
31 simp2 956 . . . . . . . . . . . . . 14 (( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) → Proj2 Proj1 y = Proj1 Proj2 x)
32 simp2 956 . . . . . . . . . . . . . 14 (( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x) → Proj2 Proj1 z = Proj1 Proj2 x)
33 eqtr3 2372 . . . . . . . . . . . . . 14 (( Proj2 Proj1 y = Proj1 Proj2 x Proj2 Proj1 z = Proj1 Proj2 x) → Proj2 Proj1 y = Proj2 Proj1 z)
3431, 32, 33syl2an 463 . . . . . . . . . . . . 13 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj2 Proj1 y = Proj2 Proj1 z)
3530, 34opeq12d 4586 . . . . . . . . . . . 12 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj1 Proj1 y, Proj2 Proj1 y = Proj1 Proj1 z, Proj2 Proj1 z)
36 opeq 4619 . . . . . . . . . . . 12 Proj1 y = Proj1 Proj1 y, Proj2 Proj1 y
37 opeq 4619 . . . . . . . . . . . 12 Proj1 z = Proj1 Proj1 z, Proj2 Proj1 z
3835, 36, 373eqtr4g 2410 . . . . . . . . . . 11 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj1 y = Proj1 z)
39 simp3 957 . . . . . . . . . . . 12 (( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) → Proj2 y = Proj2 Proj2 x)
40 simp3 957 . . . . . . . . . . . 12 (( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x) → Proj2 z = Proj2 Proj2 x)
41 eqtr3 2372 . . . . . . . . . . . 12 (( Proj2 y = Proj2 Proj2 x Proj2 z = Proj2 Proj2 x) → Proj2 y = Proj2 z)
4239, 40, 41syl2an 463 . . . . . . . . . . 11 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj2 y = Proj2 z)
4338, 42opeq12d 4586 . . . . . . . . . 10 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → Proj1 y, Proj2 y = Proj1 z, Proj2 z)
44 opeq 4619 . . . . . . . . . 10 y = Proj1 y, Proj2 y
45 opeq 4619 . . . . . . . . . 10 z = Proj1 z, Proj2 z
4643, 44, 453eqtr4g 2410 . . . . . . . . 9 ((( Proj1 Proj1 y = Proj1 x Proj2 Proj1 y = Proj1 Proj2 x Proj2 y = Proj2 Proj2 x) ( Proj1 Proj1 z = Proj1 x Proj2 Proj1 z = Proj1 Proj2 x Proj2 z = Proj2 Proj2 x)) → y = z)
4725, 26, 46syl2anb 465 . . . . . . . 8 ((y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x) → y = z)
4847gen2 1547 . . . . . . 7 yz((y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x) → y = z)
49 breq1 4642 . . . . . . . 8 (y = z → (y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))xz((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x))
5049mo4 2237 . . . . . . 7 (∃*y y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))xyz((y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x) → y = z))
5148, 50mpbir 200 . . . . . 6 ∃*y y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x
5251ax-gen 1546 . . . . 5 x∃*y y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x
53 dff12 5257 . . . . 5 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–1-1→V ↔ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–→V x∃*y y((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))x))
5424, 52, 53mpbir2an 886 . . . 4 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–1-1→V
55 ssv 3291 . . . 4 ((A × B) × C) V
56 f1ores 5300 . . . 4 ((((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )):V–1-1→V ((A × B) × C) V) → (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)))
5754, 55, 56mp2an 653 . . 3 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C))
58 vex 2862 . . . . . 6 p V
59 opeqex 4621 . . . . . 6 (p V → bc p = b, c)
60 rexcom4 2878 . . . . . . . . . . . 12 (x A py B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ px A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
61 rexcom4 2878 . . . . . . . . . . . . . 14 (y B pz C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ py B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
62 rexcom4 2878 . . . . . . . . . . . . . . . 16 (z C p(p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ pz C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
63 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 x V
64 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 y V
6563, 64opex 4588 . . . . . . . . . . . . . . . . . . . 20 x, y V
66 vex 2862 . . . . . . . . . . . . . . . . . . . 20 z V
6765, 66opex 4588 . . . . . . . . . . . . . . . . . . 19 x, y, z V
68 breq1 4642 . . . . . . . . . . . . . . . . . . 19 (p = x, y, z → (p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, cx, y, z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
6967, 68ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (p(p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ x, y, z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c)
7065, 66brco1st 5777 . . . . . . . . . . . . . . . . . . . . 21 (x, y, z(1st 1st )ax, y1st a)
7163, 64opbr1st 5501 . . . . . . . . . . . . . . . . . . . . 21 (x, y1st ax = a)
7270, 71bitri 240 . . . . . . . . . . . . . . . . . . . 20 (x, y, z(1st 1st )ax = a)
73 trtxp 5781 . . . . . . . . . . . . . . . . . . . . 21 (x, y, z((2nd 1st ) ⊗ 2nd )b, c ↔ (x, y, z(2nd 1st )b x, y, z2nd c))
74 brco 4883 . . . . . . . . . . . . . . . . . . . . . . 23 (x, y, z(2nd 1st )bt(x, y, z1st t t2nd b))
7565, 66opbr1st 5501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x, y, z1st tx, y = t)
76 eqcom 2355 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (x, y = tt = x, y)
7775, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x, y, z1st tt = x, y)
7877anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((x, y, z1st t t2nd b) ↔ (t = x, y t2nd b))
7978exbii 1582 . . . . . . . . . . . . . . . . . . . . . . 23 (t(x, y, z1st t t2nd b) ↔ t(t = x, y t2nd b))
80 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = x, y → (t2nd bx, y2nd b))
8165, 80ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 (t(t = x, y t2nd b) ↔ x, y2nd b)
8263, 64opbr2nd 5502 . . . . . . . . . . . . . . . . . . . . . . . 24 (x, y2nd by = b)
8381, 82bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = x, y t2nd b) ↔ y = b)
8474, 79, 833bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 (x, y, z(2nd 1st )by = b)
8565, 66opbr2nd 5502 . . . . . . . . . . . . . . . . . . . . . 22 (x, y, z2nd cz = c)
8684, 85anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 ((x, y, z(2nd 1st )b x, y, z2nd c) ↔ (y = b z = c))
8773, 86bitri 240 . . . . . . . . . . . . . . . . . . . 20 (x, y, z((2nd 1st ) ⊗ 2nd )b, c ↔ (y = b z = c))
8872, 87anbi12i 678 . . . . . . . . . . . . . . . . . . 19 ((x, y, z(1st 1st )a x, y, z((2nd 1st ) ⊗ 2nd )b, c) ↔ (x = a (y = b z = c)))
89 trtxp 5781 . . . . . . . . . . . . . . . . . . 19 (x, y, z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c ↔ (x, y, z(1st 1st )a x, y, z((2nd 1st ) ⊗ 2nd )b, c))
90 3anass 938 . . . . . . . . . . . . . . . . . . 19 ((x = a y = b z = c) ↔ (x = a (y = b z = c)))
9188, 89, 903bitr4i 268 . . . . . . . . . . . . . . . . . 18 (x, y, z((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c ↔ (x = a y = b z = c))
9269, 91bitri 240 . . . . . . . . . . . . . . . . 17 (p(p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (x = a y = b z = c))
9392rexbii 2639 . . . . . . . . . . . . . . . 16 (z C p(p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ z C (x = a y = b z = c))
9462, 93bitr3i 242 . . . . . . . . . . . . . . 15 (pz C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ z C (x = a y = b z = c))
9594rexbii 2639 . . . . . . . . . . . . . 14 (y B pz C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ y B z C (x = a y = b z = c))
9661, 95bitr3i 242 . . . . . . . . . . . . 13 (py B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ y B z C (x = a y = b z = c))
9796rexbii 2639 . . . . . . . . . . . 12 (x A py B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ x A y B z C (x = a y = b z = c))
9860, 97bitr3i 242 . . . . . . . . . . 11 (px A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ x A y B z C (x = a y = b z = c))
99 3reeanv 2779 . . . . . . . . . . 11 (x A y B z C (x = a y = b z = c) ↔ (x A x = a y B y = b z C z = c))
10098, 99bitri 240 . . . . . . . . . 10 (px A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (x A x = a y B y = b z C z = c))
101 r19.41v 2764 . . . . . . . . . . . 12 (x A (y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (x A y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
102 r19.41v 2764 . . . . . . . . . . . . . . 15 (z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
103102rexbii 2639 . . . . . . . . . . . . . 14 (y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ y B (z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
104 r19.41v 2764 . . . . . . . . . . . . . 14 (y B (z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
105103, 104bitri 240 . . . . . . . . . . . . 13 (y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
106105rexbii 2639 . . . . . . . . . . . 12 (x A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ x A (y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
107 elxp2 4802 . . . . . . . . . . . . . 14 (p ((A × B) × C) ↔ t (A × B)z C p = t, z)
108 df-rex 2620 . . . . . . . . . . . . . 14 (t (A × B)z C p = t, zt(t (A × B) z C p = t, z))
109 rexcom4 2878 . . . . . . . . . . . . . . 15 (x A ty B z C (t = x, y p = t, z) ↔ tx A y B z C (t = x, y p = t, z))
110 opeq1 4578 . . . . . . . . . . . . . . . . . . . . . 22 (t = x, yt, z = x, y, z)
111110eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (t = x, y → (p = t, zp = x, y, z))
11265, 111ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 (t(t = x, y p = t, z) ↔ p = x, y, z)
113112rexbii 2639 . . . . . . . . . . . . . . . . . . 19 (z C t(t = x, y p = t, z) ↔ z C p = x, y, z)
114 rexcom4 2878 . . . . . . . . . . . . . . . . . . 19 (z C t(t = x, y p = t, z) ↔ tz C (t = x, y p = t, z))
115113, 114bitr3i 242 . . . . . . . . . . . . . . . . . 18 (z C p = x, y, ztz C (t = x, y p = t, z))
116115rexbii 2639 . . . . . . . . . . . . . . . . 17 (y B z C p = x, y, zy B tz C (t = x, y p = t, z))
117 rexcom4 2878 . . . . . . . . . . . . . . . . 17 (y B tz C (t = x, y p = t, z) ↔ ty B z C (t = x, y p = t, z))
118116, 117bitri 240 . . . . . . . . . . . . . . . 16 (y B z C p = x, y, zty B z C (t = x, y p = t, z))
119118rexbii 2639 . . . . . . . . . . . . . . 15 (x A y B z C p = x, y, zx A ty B z C (t = x, y p = t, z))
120 r19.41v 2764 . . . . . . . . . . . . . . . . 17 (x A (y B t = x, y z C p = t, z) ↔ (x A y B t = x, y z C p = t, z))
121 reeanv 2778 . . . . . . . . . . . . . . . . . 18 (y B z C (t = x, y p = t, z) ↔ (y B t = x, y z C p = t, z))
122121rexbii 2639 . . . . . . . . . . . . . . . . 17 (x A y B z C (t = x, y p = t, z) ↔ x A (y B t = x, y z C p = t, z))
123 elxp2 4802 . . . . . . . . . . . . . . . . . 18 (t (A × B) ↔ x A y B t = x, y)
124123anbi1i 676 . . . . . . . . . . . . . . . . 17 ((t (A × B) z C p = t, z) ↔ (x A y B t = x, y z C p = t, z))
125120, 122, 1243bitr4ri 269 . . . . . . . . . . . . . . . 16 ((t (A × B) z C p = t, z) ↔ x A y B z C (t = x, y p = t, z))
126125exbii 1582 . . . . . . . . . . . . . . 15 (t(t (A × B) z C p = t, z) ↔ tx A y B z C (t = x, y p = t, z))
127109, 119, 1263bitr4ri 269 . . . . . . . . . . . . . 14 (t(t (A × B) z C p = t, z) ↔ x A y B z C p = x, y, z)
128107, 108, 1273bitri 262 . . . . . . . . . . . . 13 (p ((A × B) × C) ↔ x A y B z C p = x, y, z)
129128anbi1i 676 . . . . . . . . . . . 12 ((p ((A × B) × C) p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (x A y B z C p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
130101, 106, 1293bitr4ri 269 . . . . . . . . . . 11 ((p ((A × B) × C) p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ x A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
131130exbii 1582 . . . . . . . . . 10 (p(p ((A × B) × C) p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ px A y B z C (p = x, y, z p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
132 risset 2661 . . . . . . . . . . 11 (a Ax A x = a)
133 risset 2661 . . . . . . . . . . 11 (b By B y = b)
134 risset 2661 . . . . . . . . . . 11 (c Cz C z = c)
135132, 133, 1343anbi123i 1140 . . . . . . . . . 10 ((a A b B c C) ↔ (x A x = a y B y = b z C z = c))
136100, 131, 1353bitr4i 268 . . . . . . . . 9 (p(p ((A × B) × C) p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c) ↔ (a A b B c C))
137 elima2 4755 . . . . . . . . 9 (a, b, c (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ p(p ((A × B) × C) p((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd ))a, b, c))
138 opelxp 4811 . . . . . . . . . . 11 (b, c (B × C) ↔ (b B c C))
139138anbi2i 675 . . . . . . . . . 10 ((a A b, c (B × C)) ↔ (a A (b B c C)))
140 opelxp 4811 . . . . . . . . . 10 (a, b, c (A × (B × C)) ↔ (a A b, c (B × C)))
141 3anass 938 . . . . . . . . . 10 ((a A b B c C) ↔ (a A (b B c C)))
142139, 140, 1413bitr4i 268 . . . . . . . . 9 (a, b, c (A × (B × C)) ↔ (a A b B c C))
143136, 137, 1423bitr4i 268 . . . . . . . 8 (a, b, c (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, b, c (A × (B × C)))
144 opeq2 4579 . . . . . . . . . 10 (p = b, ca, p = a, b, c)
145144eleq1d 2419 . . . . . . . . 9 (p = b, c → (a, p (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, b, c (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C))))
146144eleq1d 2419 . . . . . . . . 9 (p = b, c → (a, p (A × (B × C)) ↔ a, b, c (A × (B × C))))
147145, 146bibi12d 312 . . . . . . . 8 (p = b, c → ((a, p (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, p (A × (B × C))) ↔ (a, b, c (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, b, c (A × (B × C)))))
148143, 147mpbiri 224 . . . . . . 7 (p = b, c → (a, p (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, p (A × (B × C))))
149148exlimivv 1635 . . . . . 6 (bc p = b, c → (a, p (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, p (A × (B × C))))
15058, 59, 149mp2b 9 . . . . 5 (a, p (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ a, p (A × (B × C)))
151150eqrelriv 4850 . . . 4 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) = (A × (B × C))
152 f1oeq3 5283 . . . 4 ((((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) = (A × (B × C)) → ((((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(A × (B × C))))
153151, 152ax-mp 5 . . 3 ((((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ ((A × B) × C)) ↔ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(A × (B × C)))
15457, 153mpbi 199 . 2 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(A × (B × C))
155 1stex 4739 . . . . . 6 1st V
156155, 155coex 4750 . . . . 5 (1st 1st ) V
157 2ndex 5112 . . . . . . 7 2nd V
158157, 155coex 4750 . . . . . 6 (2nd 1st ) V
159158, 157txpex 5785 . . . . 5 ((2nd 1st ) ⊗ 2nd ) V
160156, 159txpex 5785 . . . 4 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) V
161 xpassen.1 . . . . . 6 A V
162 xpassen.2 . . . . . 6 B V
163161, 162xpex 5115 . . . . 5 (A × B) V
164 xpassen.3 . . . . 5 C V
165163, 164xpex 5115 . . . 4 ((A × B) × C) V
166160, 165resex 5117 . . 3 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)) V
167166f1oen 6033 . 2 ((((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) ((A × B) × C)):((A × B) × C)–1-1-onto→(A × (B × C)) → ((A × B) × C) ≈ (A × (B × C)))
168154, 167ax-mp 5 1 ((A × B) × C) ≈ (A × (B × C))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358   w3a 934  wal 1540  wex 1541   = wceq 1642   wcel 1710  ∃*wmo 2205  wrex 2615  Vcvv 2859  cin 3208   wss 3257  cop 4561   Proj1 cproj1 4563   Proj2 cproj2 4564   class class class wbr 4639  1st c1st 4717   ccom 4721  cima 4722   × cxp 4770  ran crn 4773   cres 4774   Fn wfn 4776  –→wf 4777  1-1wf1 4778  ontowfo 4779  1-1-ontowf1o 4780  2nd c2nd 4783  ctxp 5735  cen 6028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-co 4726  df-ima 4727  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-2nd 4797  df-txp 5736  df-en 6029
This theorem is referenced by:  mucass  6135
  Copyright terms: Public domain W3C validator