crossex - New Foundations Explorer

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

Theorem crossex 5851

Description: The function mapping x and y to their cross product is a set. (Contributed by SF, 11-Feb-2015.)

**Assertion**
Ref	Expression
crossex	⊢ Cross ∈ V

Proof of Theorem crossex Dummy variables a b x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cross 5765	. . 3 ⊢ Cross = (x ∈ V, y ∈ V ↦ (x × y))
2		rexcom 2773	. . . . 5 ⊢ (∃a ∈ x ∃b ∈ y z = ⟨a, b⟩ ↔ ∃b ∈ y ∃a ∈ x z = ⟨a, b⟩)
3		elxp2 4803	. . . . 5 ⊢ (z ∈ (x × y) ↔ ∃a ∈ x ∃b ∈ y z = ⟨a, b⟩)
4		elin 3220	. . . . . . . 8 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) ↔ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)))
5		snex 4112	. . . . . . . . . . 11 ⊢ {z} ∈ V
6	5	otelins2 5792	. . . . . . . . . 10 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{b}, ⟨x, y⟩⟩ ∈ Ins2 S )
7		vex 2863	. . . . . . . . . . 11 ⊢ x ∈ V
8	7	otelins2 5792	. . . . . . . . . 10 ⊢ (⟨{b}, ⟨x, y⟩⟩ ∈ Ins2 S ↔ ⟨{b}, y⟩ ∈ S )
9		vex 2863	. . . . . . . . . . 11 ⊢ b ∈ V
10		vex 2863	. . . . . . . . . . 11 ⊢ y ∈ V
11	9, 10	opelssetsn 4761	. . . . . . . . . 10 ⊢ (⟨{b}, y⟩ ∈ S ↔ b ∈ y)
12	6, 8, 11	3bitri 262	. . . . . . . . 9 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins2 Ins2 S ↔ b ∈ y)
13	10	oqelins4 5795	. . . . . . . . . 10 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ↔ ⟨{b}, ⟨{z}, x⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c))
14		elin 3220	. . . . . . . . . . . . 13 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) ↔ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))))
15		snex 4112	. . . . . . . . . . . . . . . 16 ⊢ {b} ∈ V
16	15	otelins2 5792	. . . . . . . . . . . . . . 15 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{a}, ⟨{z}, x⟩⟩ ∈ Ins2 S )
17	5	otelins2 5792	. . . . . . . . . . . . . . 15 ⊢ (⟨{a}, ⟨{z}, x⟩⟩ ∈ Ins2 S ↔ ⟨{a}, x⟩ ∈ S )
18		vex 2863	. . . . . . . . . . . . . . . 16 ⊢ a ∈ V
19	18, 7	opelssetsn 4761	. . . . . . . . . . . . . . 15 ⊢ (⟨{a}, x⟩ ∈ S ↔ a ∈ x)
20	16, 17, 19	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins2 Ins2 S ↔ a ∈ x)
21	7	oqelins4 5795	. . . . . . . . . . . . . . 15 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ↔ ⟨{a}, ⟨{b}, {z}⟩⟩ ∈ SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )))
22		vex 2863	. . . . . . . . . . . . . . . 16 ⊢ z ∈ V
23	18, 9, 22	otsnelsi3 5806	. . . . . . . . . . . . . . 15 ⊢ (⟨{a}, ⟨{b}, {z}⟩⟩ ∈ SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ↔ ⟨a, ⟨b, z⟩⟩ ∈ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )))
24		elin 3220	. . . . . . . . . . . . . . . 16 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ↔ (⟨a, ⟨b, z⟩⟩ ∈ Ins2 ^◡1^st ∧ ⟨a, ⟨b, z⟩⟩ ∈ (V × ^◡2^nd )))
25	9	otelins2 5792	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ Ins2 ^◡1^st ↔ ⟨a, z⟩ ∈ ^◡1^st )
26		df-br 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (a^◡1^st z ↔ ⟨a, z⟩ ∈ ^◡1^st )
27		brcnv 4893	. . . . . . . . . . . . . . . . . 18 ⊢ (a^◡1^st z ↔ z1^st a)
28	25, 26, 27	3bitr2i 264	. . . . . . . . . . . . . . . . 17 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ Ins2 ^◡1^st ↔ z1^st a)
29		opelxp 4812	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ (V × ^◡2^nd ) ↔ (a ∈ V ∧ ⟨b, z⟩ ∈ ^◡2^nd ))
30	18, 29	mpbiran 884	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ (V × ^◡2^nd ) ↔ ⟨b, z⟩ ∈ ^◡2^nd )
31		df-br 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (b^◡2^nd z ↔ ⟨b, z⟩ ∈ ^◡2^nd )
32		brcnv 4893	. . . . . . . . . . . . . . . . . 18 ⊢ (b^◡2^nd z ↔ z2^nd b)
33	30, 31, 32	3bitr2i 264	. . . . . . . . . . . . . . . . 17 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ (V × ^◡2^nd ) ↔ z2^nd b)
34	28, 33	anbi12i 678	. . . . . . . . . . . . . . . 16 ⊢ ((⟨a, ⟨b, z⟩⟩ ∈ Ins2 ^◡1^st ∧ ⟨a, ⟨b, z⟩⟩ ∈ (V × ^◡2^nd )) ↔ (z1^st a ∧ z2^nd b))
35	18, 9	op1st2nd 5791	. . . . . . . . . . . . . . . 16 ⊢ ((z1^st a ∧ z2^nd b) ↔ z = ⟨a, b⟩)
36	24, 34, 35	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (⟨a, ⟨b, z⟩⟩ ∈ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ↔ z = ⟨a, b⟩)
37	21, 23, 36	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ↔ z = ⟨a, b⟩)
38	20, 37	anbi12i 678	. . . . . . . . . . . . 13 ⊢ ((⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) ↔ (a ∈ x ∧ z = ⟨a, b⟩))
39	14, 38	bitri 240	. . . . . . . . . . . 12 ⊢ (⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) ↔ (a ∈ x ∧ z = ⟨a, b⟩))
40	39	exbii 1582	. . . . . . . . . . 11 ⊢ (∃a⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) ↔ ∃a(a ∈ x ∧ z = ⟨a, b⟩))
41		elima1c 4948	. . . . . . . . . . 11 ⊢ (⟨{b}, ⟨{z}, x⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ↔ ∃a⟨{a}, ⟨{b}, ⟨{z}, x⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))))
42		df-rex 2621	. . . . . . . . . . 11 ⊢ (∃a ∈ x z = ⟨a, b⟩ ↔ ∃a(a ∈ x ∧ z = ⟨a, b⟩))
43	40, 41, 42	3bitr4i 268	. . . . . . . . . 10 ⊢ (⟨{b}, ⟨{z}, x⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ↔ ∃a ∈ x z = ⟨a, b⟩)
44	13, 43	bitri 240	. . . . . . . . 9 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ↔ ∃a ∈ x z = ⟨a, b⟩)
45	12, 44	anbi12i 678	. . . . . . . 8 ⊢ ((⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) ↔ (b ∈ y ∧ ∃a ∈ x z = ⟨a, b⟩))
46	4, 45	bitri 240	. . . . . . 7 ⊢ (⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) ↔ (b ∈ y ∧ ∃a ∈ x z = ⟨a, b⟩))
47	46	exbii 1582	. . . . . 6 ⊢ (∃b⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) ↔ ∃b(b ∈ y ∧ ∃a ∈ x z = ⟨a, b⟩))
48		elima1c 4948	. . . . . 6 ⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c) ↔ ∃b⟨{b}, ⟨{z}, ⟨x, y⟩⟩⟩ ∈ ( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)))
49		df-rex 2621	. . . . . 6 ⊢ (∃b ∈ y ∃a ∈ x z = ⟨a, b⟩ ↔ ∃b(b ∈ y ∧ ∃a ∈ x z = ⟨a, b⟩))
50	47, 48, 49	3bitr4i 268	. . . . 5 ⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c) ↔ ∃b ∈ y ∃a ∈ x z = ⟨a, b⟩)
51	2, 3, 50	3bitr4ri 269	. . . 4 ⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c) ↔ z ∈ (x × y))
52	51	releqmpt2 5810	. . 3 ⊢ (((V × V) × V) ∖ (( Ins2 S ⊕ Ins3 (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c)) “ 1_c)) = (x ∈ V, y ∈ V ↦ (x × y))
53	1, 52	eqtr4i 2376	. 2 ⊢ Cross = (((V × V) × V) ∖ (( Ins2 S ⊕ Ins3 (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c)) “ 1_c))
54		vvex 4110	. . 3 ⊢ V ∈ V
55		ssetex 4745	. . . . . . 7 ⊢ S ∈ V
56	55	ins2ex 5798	. . . . . 6 ⊢ Ins2 S ∈ V
57	56	ins2ex 5798	. . . . 5 ⊢ Ins2 Ins2 S ∈ V
58		1stex 4740	. . . . . . . . . . . . 13 ⊢ 1^st ∈ V
59	58	cnvex 5103	. . . . . . . . . . . 12 ⊢ ^◡1^st ∈ V
60	59	ins2ex 5798	. . . . . . . . . . 11 ⊢ Ins2 ^◡1^st ∈ V
61		2ndex 5113	. . . . . . . . . . . . 13 ⊢ 2^nd ∈ V
62	61	cnvex 5103	. . . . . . . . . . . 12 ⊢ ^◡2^nd ∈ V
63	54, 62	xpex 5116	. . . . . . . . . . 11 ⊢ (V × ^◡2^nd ) ∈ V
64	60, 63	inex 4106	. . . . . . . . . 10 ⊢ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ∈ V
65	64	si3ex 5807	. . . . . . . . 9 ⊢ SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ∈ V
66	65	ins4ex 5800	. . . . . . . 8 ⊢ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd )) ∈ V
67	57, 66	inex 4106	. . . . . . 7 ⊢ ( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) ∈ V
68		1cex 4143	. . . . . . 7 ⊢ 1_c ∈ V
69	67, 68	imaex 4748	. . . . . 6 ⊢ (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ∈ V
70	69	ins4ex 5800	. . . . 5 ⊢ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c) ∈ V
71	57, 70	inex 4106	. . . 4 ⊢ ( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) ∈ V
72	71, 68	imaex 4748	. . 3 ⊢ (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c) ∈ V
73	54, 54, 72	mpt2exlem 5812	. 2 ⊢ (((V × V) × V) ∖ (( Ins2 S ⊕ Ins3 (( Ins2 Ins2 S ∩ Ins4 (( Ins2 Ins2 S ∩ Ins4 SI₃ ( Ins2 ^◡1^st ∩ (V × ^◡2^nd ))) “ 1_c)) “ 1_c)) “ 1_c)) ∈ V
74	53, 73	eqeltri 2423	1 ⊢ Cross ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 358 ∃wex 1541 = wceq 1642 ∈ wcel 1710 ∃wrex 2616 Vcvv 2860 ∖ cdif 3207 ∩ cin 3209 ⊕ csymdif 3210 {csn 3738 1_cc1c 4135 ⟨cop 4562 class class class wbr 4640 1^st c1st 4718 S csset 4720 “ cima 4723 × cxp 4771 ^◡ccnv 4772 2^nd c2nd 4784 ↦ cmpt2 5654 Ins2 cins2 5750 Ins3 cins3 5752 Ins4 cins4 5756 SI₃ csi3 5758 Cross ccross 5764

This proof depends on 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 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This proof 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 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-xp 4785 df-cnv 4786 df-2nd 4798 df-oprab 5529 df-mpt2 5655 df-txp 5737 df-ins2 5751 df-ins3 5753 df-ins4 5757 df-si3 5759 df-cross 5765

This theorem is used by: ovmuc 6131 mucex 6134

W3C validator