Theorem usgrexmplef

Description: Lemma for usgrexmpl . (Contributed by Alexander van der Vekens, 15-Aug-2017)

	Ref	Expression
Hypotheses	usgrexmplef.v	$$⊢V=\left(0\dots 4\right)$$
	usgrexmplef.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
Assertion	usgrexmplef	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexmplef.v	$$⊢V=\left(0\dots 4\right)$$
2		usgrexmplef.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
3		usgrexmpldifpr	$$⊢\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,0\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{2,0\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{2,0\right\}\ne \left\{0,3\right\}\right)\right)$$
4		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
5		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
6		prex	$$⊢\left\{2,0\right\}\in \mathrm{V}$$
7		prex	$$⊢\left\{0,3\right\}\in \mathrm{V}$$
8		s4f1o	$$⊢\left(\left(\left\{0,1\right\}\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\right)\wedge \left(\left\{2,0\right\}\in \mathrm{V}\wedge \left\{0,3\right\}\in \mathrm{V}\right)\right)\to \left(\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,0\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{2,0\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{2,0\right\}\ne \left\{0,3\right\}\right)\right)\to \left(E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)\right)$$
9	4 5 6 7 8	mp4an	$$⊢\left(\left(\left\{0,1\right\}\ne \left\{1,2\right\}\wedge \left\{0,1\right\}\ne \left\{2,0\right\}\wedge \left\{0,1\right\}\ne \left\{0,3\right\}\right)\wedge \left(\left\{1,2\right\}\ne \left\{2,0\right\}\wedge \left\{1,2\right\}\ne \left\{0,3\right\}\wedge \left\{2,0\right\}\ne \left\{0,3\right\}\right)\right)\to \left(E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩\to E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)$$
10	3 2 9	mp2	$$⊢E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}$$
11		f1of1	$$⊢E:\mathrm{dom}E\underset{1-1\; onto}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}$$
12		id	$$⊢\mathrm{ran}E\subseteq \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to \mathrm{ran}E\subseteq \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}$$
13		vex	$$⊢p\in \mathrm{V}$$
14	13	elpr	$$⊢p\in \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\leftrightarrow \left(p=\left\{0,1\right\}\vee p=\left\{1,2\right\}\right)$$
15		0nn0	$$⊢0\in {\mathbb{N}}_0$$
16		4nn0	$$⊢4\in {\mathbb{N}}_0$$
17		0re	$$⊢0\in ℝ$$
18		4re	$$⊢4\in ℝ$$
19		4pos	$$⊢0<4$$
20	17 18 19	ltleii	$$⊢0\le 4$$
21		elfz2nn0	$$⊢0\in \left(0\dots 4\right)\leftrightarrow \left(0\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\wedge 0\le 4\right)$$
22	15 16 20 21	mpbir3an	$$⊢0\in \left(0\dots 4\right)$$
23	22 1	eleqtrri	$$⊢0\in V$$
24		1nn0	$$⊢1\in {\mathbb{N}}_0$$
25		1re	$$⊢1\in ℝ$$
26		1lt4	$$⊢1<4$$
27	25 18 26	ltleii	$$⊢1\le 4$$
28		elfz2nn0	$$⊢1\in \left(0\dots 4\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\wedge 1\le 4\right)$$
29	24 16 27 28	mpbir3an	$$⊢1\in \left(0\dots 4\right)$$
30	29 1	eleqtrri	$$⊢1\in V$$
31		prelpwi	$$⊢\left(0\in V\wedge 1\in V\right)\to \left\{0,1\right\}\in 𝒫V$$
32		eleq1	$$⊢p=\left\{0,1\right\}\to \left(p\in 𝒫V\leftrightarrow \left\{0,1\right\}\in 𝒫V\right)$$
33	31 32	syl5ibrcom	$$⊢\left(0\in V\wedge 1\in V\right)\to \left(p=\left\{0,1\right\}\to p\in 𝒫V\right)$$
34	23 30 33	mp2an	$$⊢p=\left\{0,1\right\}\to p\in 𝒫V$$
35		fveq2	$$⊢p=\left\{0,1\right\}\to \left|p\right|=\left|\left\{0,1\right\}\right|$$
36		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
37	35 36	eqtrdi	$$⊢p=\left\{0,1\right\}\to \left|p\right|=2$$
38	34 37	jca	$$⊢p=\left\{0,1\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
39		2nn0	$$⊢2\in {\mathbb{N}}_0$$
40		2re	$$⊢2\in ℝ$$
41		2lt4	$$⊢2<4$$
42	40 18 41	ltleii	$$⊢2\le 4$$
43		elfz2nn0	$$⊢2\in \left(0\dots 4\right)\leftrightarrow \left(2\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\wedge 2\le 4\right)$$
44	39 16 42 43	mpbir3an	$$⊢2\in \left(0\dots 4\right)$$
45	44 1	eleqtrri	$$⊢2\in V$$
46		prelpwi	$$⊢\left(1\in V\wedge 2\in V\right)\to \left\{1,2\right\}\in 𝒫V$$
47		eleq1	$$⊢p=\left\{1,2\right\}\to \left(p\in 𝒫V\leftrightarrow \left\{1,2\right\}\in 𝒫V\right)$$
48	46 47	syl5ibrcom	$$⊢\left(1\in V\wedge 2\in V\right)\to \left(p=\left\{1,2\right\}\to p\in 𝒫V\right)$$
49	30 45 48	mp2an	$$⊢p=\left\{1,2\right\}\to p\in 𝒫V$$
50		fveq2	$$⊢p=\left\{1,2\right\}\to \left|p\right|=\left|\left\{1,2\right\}\right|$$
51		1ne2	$$⊢1\ne 2$$
52		1nn	$$⊢1\in \mathbb{N}$$
53		2nn	$$⊢2\in \mathbb{N}$$
54		hashprg	$$⊢\left(1\in \mathbb{N}\wedge 2\in \mathbb{N}\right)\to \left(1\ne 2\leftrightarrow \left|\left\{1,2\right\}\right|=2\right)$$
55	52 53 54	mp2an	$$⊢1\ne 2\leftrightarrow \left|\left\{1,2\right\}\right|=2$$
56	51 55	mpbi	$$⊢\left|\left\{1,2\right\}\right|=2$$
57	50 56	eqtrdi	$$⊢p=\left\{1,2\right\}\to \left|p\right|=2$$
58	49 57	jca	$$⊢p=\left\{1,2\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
59	38 58	jaoi	$$⊢\left(p=\left\{0,1\right\}\vee p=\left\{1,2\right\}\right)\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
60	14 59	sylbi	$$⊢p\in \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
61	13	elpr	$$⊢p\in \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\leftrightarrow \left(p=\left\{2,0\right\}\vee p=\left\{0,3\right\}\right)$$
62		prelpwi	$$⊢\left(2\in V\wedge 0\in V\right)\to \left\{2,0\right\}\in 𝒫V$$
63		eleq1	$$⊢p=\left\{2,0\right\}\to \left(p\in 𝒫V\leftrightarrow \left\{2,0\right\}\in 𝒫V\right)$$
64	62 63	syl5ibrcom	$$⊢\left(2\in V\wedge 0\in V\right)\to \left(p=\left\{2,0\right\}\to p\in 𝒫V\right)$$
65	45 23 64	mp2an	$$⊢p=\left\{2,0\right\}\to p\in 𝒫V$$
66		fveq2	$$⊢p=\left\{2,0\right\}\to \left|p\right|=\left|\left\{2,0\right\}\right|$$
67		2ne0	$$⊢2\ne 0$$
68		2z	$$⊢2\in \mathbb{Z}$$
69		0z	$$⊢0\in \mathbb{Z}$$
70		hashprg	$$⊢\left(2\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to \left(2\ne 0\leftrightarrow \left|\left\{2,0\right\}\right|=2\right)$$
71	68 69 70	mp2an	$$⊢2\ne 0\leftrightarrow \left|\left\{2,0\right\}\right|=2$$
72	67 71	mpbi	$$⊢\left|\left\{2,0\right\}\right|=2$$
73	66 72	eqtrdi	$$⊢p=\left\{2,0\right\}\to \left|p\right|=2$$
74	65 73	jca	$$⊢p=\left\{2,0\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
75		3nn0	$$⊢3\in {\mathbb{N}}_0$$
76		3re	$$⊢3\in ℝ$$
77		3lt4	$$⊢3<4$$
78	76 18 77	ltleii	$$⊢3\le 4$$
79		elfz2nn0	$$⊢3\in \left(0\dots 4\right)\leftrightarrow \left(3\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\wedge 3\le 4\right)$$
80	75 16 78 79	mpbir3an	$$⊢3\in \left(0\dots 4\right)$$
81	80 1	eleqtrri	$$⊢3\in V$$
82		prelpwi	$$⊢\left(0\in V\wedge 3\in V\right)\to \left\{0,3\right\}\in 𝒫V$$
83		eleq1	$$⊢p=\left\{0,3\right\}\to \left(p\in 𝒫V\leftrightarrow \left\{0,3\right\}\in 𝒫V\right)$$
84	82 83	syl5ibrcom	$$⊢\left(0\in V\wedge 3\in V\right)\to \left(p=\left\{0,3\right\}\to p\in 𝒫V\right)$$
85	23 81 84	mp2an	$$⊢p=\left\{0,3\right\}\to p\in 𝒫V$$
86		fveq2	$$⊢p=\left\{0,3\right\}\to \left|p\right|=\left|\left\{0,3\right\}\right|$$
87		3ne0	$$⊢3\ne 0$$
88	87	necomi	$$⊢0\ne 3$$
89		3z	$$⊢3\in \mathbb{Z}$$
90		hashprg	$$⊢\left(0\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to \left(0\ne 3\leftrightarrow \left|\left\{0,3\right\}\right|=2\right)$$
91	69 89 90	mp2an	$$⊢0\ne 3\leftrightarrow \left|\left\{0,3\right\}\right|=2$$
92	88 91	mpbi	$$⊢\left|\left\{0,3\right\}\right|=2$$
93	86 92	eqtrdi	$$⊢p=\left\{0,3\right\}\to \left|p\right|=2$$
94	85 93	jca	$$⊢p=\left\{0,3\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
95	74 94	jaoi	$$⊢\left(p=\left\{2,0\right\}\vee p=\left\{0,3\right\}\right)\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
96	61 95	sylbi	$$⊢p\in \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
97	60 96	jaoi	$$⊢\left(p\in \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\vee p\in \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)\to \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
98		elun	$$⊢p\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)\leftrightarrow \left(p\in \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\vee p\in \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)$$
99		fveqeq2	$$⊢e=p\to \left(\left|e\right|=2\leftrightarrow \left|p\right|=2\right)$$
100	99	elrab	$$⊢p\in \left\{e\in 𝒫V|\left|e\right|=2\right\}\leftrightarrow \left(p\in 𝒫V\wedge \left|p\right|=2\right)$$
101	97 98 100	3imtr4i	$$⊢p\in \left(\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)\to p\in \left\{e\in 𝒫V|\left|e\right|=2\right\}$$
102	101	ssriv	$$⊢\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}$$
103	12 102	sstrdi	$$⊢\mathrm{ran}E\subseteq \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to \mathrm{ran}E\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}$$
104	103	anim2i	$$⊢\left(EFn\mathrm{dom}E\wedge \mathrm{ran}E\subseteq \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)\to \left(EFn\mathrm{dom}E\wedge \mathrm{ran}E\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}\right)$$
105		df-f	$$⊢E:\mathrm{dom}E⟶\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\leftrightarrow \left(EFn\mathrm{dom}E\wedge \mathrm{ran}E\subseteq \left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\right)$$
106		df-f	$$⊢E:\mathrm{dom}E⟶\left\{e\in 𝒫V|\left|e\right|=2\right\}\leftrightarrow \left(EFn\mathrm{dom}E\wedge \mathrm{ran}E\subseteq \left\{e\in 𝒫V|\left|e\right|=2\right\}\right)$$
107	104 105 106	3imtr4i	$$⊢E:\mathrm{dom}E⟶\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to E:\mathrm{dom}E⟶\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
108	107	anim1i	$$⊢\left(E:\mathrm{dom}E⟶\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\wedge \forall x{\exists }^{*}yyEx\right)\to \left(E:\mathrm{dom}E⟶\left\{e\in 𝒫V|\left|e\right|=2\right\}\wedge \forall x{\exists }^{*}yyEx\right)$$
109		dff12	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\leftrightarrow \left(E:\mathrm{dom}E⟶\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\wedge \forall x{\exists }^{*}yyEx\right)$$
110		dff12	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}\leftrightarrow \left(E:\mathrm{dom}E⟶\left\{e\in 𝒫V|\left|e\right|=2\right\}\wedge \forall x{\exists }^{*}yyEx\right)$$
111	108 109 110	3imtr4i	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{\left\{0,1\right\},\left\{1,2\right\}\right\}\cup \left\{\left\{2,0\right\},\left\{0,3\right\}\right\}\to E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$
112	10 11 111	mp2b	$$⊢E:\mathrm{dom}E\underset{1-1}{⟶}\left\{e\in 𝒫V|\left|e\right|=2\right\}$$