# Metamath Proof Explorer

## 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\}↔\left({p}=\left\{0,1\right\}\vee {p}=\left\{1,2\right\}\right)$
15 0nn0 ${⊢}0\in {ℕ}_{0}$
16 4nn0 ${⊢}4\in {ℕ}_{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)↔\left(0\in {ℕ}_{0}\wedge 4\in {ℕ}_{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 {ℕ}_{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)↔\left(1\in {ℕ}_{0}\wedge 4\in {ℕ}_{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}↔\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 syl6eq ${⊢}{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 {ℕ}_{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)↔\left(2\in {ℕ}_{0}\wedge 4\in {ℕ}_{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}↔\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 ℕ$
53 2nn ${⊢}2\in ℕ$
54 hashprg ${⊢}\left(1\in ℕ\wedge 2\in ℕ\right)\to \left(1\ne 2↔\left|\left\{1,2\right\}\right|=2\right)$
55 52 53 54 mp2an ${⊢}1\ne 2↔\left|\left\{1,2\right\}\right|=2$
56 51 55 mpbi ${⊢}\left|\left\{1,2\right\}\right|=2$
57 50 56 syl6eq ${⊢}{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\}↔\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}↔\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 ℤ$
69 0z ${⊢}0\in ℤ$
70 hashprg ${⊢}\left(2\in ℤ\wedge 0\in ℤ\right)\to \left(2\ne 0↔\left|\left\{2,0\right\}\right|=2\right)$
71 68 69 70 mp2an ${⊢}2\ne 0↔\left|\left\{2,0\right\}\right|=2$
72 67 71 mpbi ${⊢}\left|\left\{2,0\right\}\right|=2$
73 66 72 syl6eq ${⊢}{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 {ℕ}_{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)↔\left(3\in {ℕ}_{0}\wedge 4\in {ℕ}_{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}↔\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 ℤ$
90 hashprg ${⊢}\left(0\in ℤ\wedge 3\in ℤ\right)\to \left(0\ne 3↔\left|\left\{0,3\right\}\right|=2\right)$
91 69 89 90 mp2an ${⊢}0\ne 3↔\left|\left\{0,3\right\}\right|=2$
92 88 91 mpbi ${⊢}\left|\left\{0,3\right\}\right|=2$
93 86 92 syl6eq ${⊢}{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)↔\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↔\left|{p}\right|=2\right)$
100 99 elrab ${⊢}{p}\in \left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}↔\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({E}Fn\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({E}Fn\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\}↔\left({E}Fn\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\}↔\left({E}Fn\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}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{E}{x}\right)\to \left({E}:\mathrm{dom}{E}⟶\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{E}{x}\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\}↔\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}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{E}{x}\right)$
110 dff12 ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}↔\left({E}:\mathrm{dom}{E}⟶\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{E}{x}\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\}$