Metamath Proof Explorer

Theorem fi1uzind

Description: Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses fi1uzind.f ${⊢}{F}\in \mathrm{V}$
fi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
fi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
fi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
fi1uzind.3
fi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
fi1uzind.base
fi1uzind.step
Assertion fi1uzind

Proof

Step Hyp Ref Expression
1 fi1uzind.f ${⊢}{F}\in \mathrm{V}$
2 fi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
3 fi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
4 fi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
5 fi1uzind.3
6 fi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
7 fi1uzind.base
8 fi1uzind.step
9 dfclel ${⊢}\left|{V}\right|\in {ℕ}_{0}↔\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}=\left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)$
10 nn0z ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℤ$
11 2 10 mp1i ${⊢}\left(\left({L}\le \left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\wedge {n}=\left|{V}\right|\right)\to {L}\in ℤ$
12 nn0z ${⊢}{n}\in {ℕ}_{0}\to {n}\in ℤ$
13 12 ad2antlr ${⊢}\left(\left({L}\le \left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\wedge {n}=\left|{V}\right|\right)\to {n}\in ℤ$
14 breq2 ${⊢}\left|{V}\right|={n}\to \left({L}\le \left|{V}\right|↔{L}\le {n}\right)$
15 14 eqcoms ${⊢}{n}=\left|{V}\right|\to \left({L}\le \left|{V}\right|↔{L}\le {n}\right)$
16 15 biimpcd ${⊢}{L}\le \left|{V}\right|\to \left({n}=\left|{V}\right|\to {L}\le {n}\right)$
17 16 adantr ${⊢}\left({L}\le \left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\to \left({n}=\left|{V}\right|\to {L}\le {n}\right)$
18 17 imp ${⊢}\left(\left({L}\le \left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\wedge {n}=\left|{V}\right|\right)\to {L}\le {n}$
19 eqeq1 ${⊢}{x}={L}\to \left({x}=\left|{v}\right|↔{L}=\left|{v}\right|\right)$
20 19 anbi2d
21 20 imbi1d
22 21 2albidv
23 eqeq1 ${⊢}{x}={y}\to \left({x}=\left|{v}\right|↔{y}=\left|{v}\right|\right)$
24 23 anbi2d
25 24 imbi1d
26 25 2albidv
27 eqeq1 ${⊢}{x}={y}+1\to \left({x}=\left|{v}\right|↔{y}+1=\left|{v}\right|\right)$
28 27 anbi2d
29 28 imbi1d
30 29 2albidv
31 eqeq1 ${⊢}{x}={n}\to \left({x}=\left|{v}\right|↔{n}=\left|{v}\right|\right)$
32 31 anbi2d
33 32 imbi1d
34 33 2albidv
35 eqcom ${⊢}{L}=\left|{v}\right|↔\left|{v}\right|={L}$
36 35 7 sylan2b
37 36 gen2
38 37 a1i
39 simpl ${⊢}\left({v}={w}\wedge {e}={f}\right)\to {v}={w}$
40 simpr ${⊢}\left({v}={w}\wedge {e}={f}\right)\to {e}={f}$
41 40 sbceq1d
42 39 41 sbceqbid
43 fveq2 ${⊢}{v}={w}\to \left|{v}\right|=\left|{w}\right|$
44 43 eqeq2d ${⊢}{v}={w}\to \left({y}=\left|{v}\right|↔{y}=\left|{w}\right|\right)$
45 44 adantr ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({y}=\left|{v}\right|↔{y}=\left|{w}\right|\right)$
46 42 45 anbi12d
47 46 4 imbi12d
48 47 cbval2vw
49 nn0ge0 ${⊢}{L}\in {ℕ}_{0}\to 0\le {L}$
50 0red ${⊢}{y}\in ℤ\to 0\in ℝ$
51 nn0re ${⊢}{L}\in {ℕ}_{0}\to {L}\in ℝ$
52 2 51 mp1i ${⊢}{y}\in ℤ\to {L}\in ℝ$
53 zre ${⊢}{y}\in ℤ\to {y}\in ℝ$
54 letr ${⊢}\left(0\in ℝ\wedge {L}\in ℝ\wedge {y}\in ℝ\right)\to \left(\left(0\le {L}\wedge {L}\le {y}\right)\to 0\le {y}\right)$
55 50 52 53 54 syl3anc ${⊢}{y}\in ℤ\to \left(\left(0\le {L}\wedge {L}\le {y}\right)\to 0\le {y}\right)$
56 0nn0 ${⊢}0\in {ℕ}_{0}$
57 pm3.22 ${⊢}\left(0\le {y}\wedge {y}\in ℤ\right)\to \left({y}\in ℤ\wedge 0\le {y}\right)$
58 0z ${⊢}0\in ℤ$
59 eluz1 ${⊢}0\in ℤ\to \left({y}\in {ℤ}_{\ge 0}↔\left({y}\in ℤ\wedge 0\le {y}\right)\right)$
60 58 59 mp1i ${⊢}\left(0\le {y}\wedge {y}\in ℤ\right)\to \left({y}\in {ℤ}_{\ge 0}↔\left({y}\in ℤ\wedge 0\le {y}\right)\right)$
61 57 60 mpbird ${⊢}\left(0\le {y}\wedge {y}\in ℤ\right)\to {y}\in {ℤ}_{\ge 0}$
62 eluznn0 ${⊢}\left(0\in {ℕ}_{0}\wedge {y}\in {ℤ}_{\ge 0}\right)\to {y}\in {ℕ}_{0}$
63 56 61 62 sylancr ${⊢}\left(0\le {y}\wedge {y}\in ℤ\right)\to {y}\in {ℕ}_{0}$
64 63 ex ${⊢}0\le {y}\to \left({y}\in ℤ\to {y}\in {ℕ}_{0}\right)$
65 55 64 syl6com ${⊢}\left(0\le {L}\wedge {L}\le {y}\right)\to \left({y}\in ℤ\to \left({y}\in ℤ\to {y}\in {ℕ}_{0}\right)\right)$
66 65 ex ${⊢}0\le {L}\to \left({L}\le {y}\to \left({y}\in ℤ\to \left({y}\in ℤ\to {y}\in {ℕ}_{0}\right)\right)\right)$
67 66 com14 ${⊢}{y}\in ℤ\to \left({L}\le {y}\to \left({y}\in ℤ\to \left(0\le {L}\to {y}\in {ℕ}_{0}\right)\right)\right)$
68 67 pm2.43a ${⊢}{y}\in ℤ\to \left({L}\le {y}\to \left(0\le {L}\to {y}\in {ℕ}_{0}\right)\right)$
69 68 imp ${⊢}\left({y}\in ℤ\wedge {L}\le {y}\right)\to \left(0\le {L}\to {y}\in {ℕ}_{0}\right)$
70 69 com12 ${⊢}0\le {L}\to \left(\left({y}\in ℤ\wedge {L}\le {y}\right)\to {y}\in {ℕ}_{0}\right)$
71 2 49 70 mp2b ${⊢}\left({y}\in ℤ\wedge {L}\le {y}\right)\to {y}\in {ℕ}_{0}$
72 71 3adant1 ${⊢}\left({L}\in ℤ\wedge {y}\in ℤ\wedge {L}\le {y}\right)\to {y}\in {ℕ}_{0}$
73 eqcom ${⊢}{y}+1=\left|{v}\right|↔\left|{v}\right|={y}+1$
74 nn0p1gt0 ${⊢}{y}\in {ℕ}_{0}\to 0<{y}+1$
75 74 adantr ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to 0<{y}+1$
76 simpr ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to \left|{v}\right|={y}+1$
77 75 76 breqtrrd ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to 0<\left|{v}\right|$
78 73 77 sylan2b ${⊢}\left({y}\in {ℕ}_{0}\wedge {y}+1=\left|{v}\right|\right)\to 0<\left|{v}\right|$
80 hashgt0elex ${⊢}\left({v}\in \mathrm{V}\wedge 0<\left|{v}\right|\right)\to \exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {v}$
81 vex ${⊢}{v}\in \mathrm{V}$
82 81 a1i ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {v}\in \mathrm{V}$
83 simpr ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {n}\in {v}$
84 simpl ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {y}\in {ℕ}_{0}$
85 hashdifsnp1 ${⊢}\left({v}\in \mathrm{V}\wedge {n}\in {v}\wedge {y}\in {ℕ}_{0}\right)\to \left(\left|{v}\right|={y}+1\to \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
86 73 85 syl5bi ${⊢}\left({v}\in \mathrm{V}\wedge {n}\in {v}\wedge {y}\in {ℕ}_{0}\right)\to \left({y}+1=\left|{v}\right|\to \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
87 82 83 84 86 syl3anc ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to \left({y}+1=\left|{v}\right|\to \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
88 87 imp ${⊢}\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge {y}+1=\left|{v}\right|\right)\to \left|{v}\setminus \left\{{n}\right\}\right|={y}$
89 peano2nn0 ${⊢}{y}\in {ℕ}_{0}\to {y}+1\in {ℕ}_{0}$
90 89 ad2antrr ${⊢}\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge {y}+1=\left|{v}\right|\right)\to {y}+1\in {ℕ}_{0}$
92 simpr
93 simplrr
94 simprlr
96 92 93 95 3jca
97 91 96 jca
98 81 difexi ${⊢}{v}\setminus \left\{{n}\right\}\in \mathrm{V}$
99 simpl ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to {w}={v}\setminus \left\{{n}\right\}$
100 simpr ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to {f}={F}$
101 100 sbceq1d
102 99 101 sbceqbid
103 eqcom ${⊢}{y}=\left|{w}\right|↔\left|{w}\right|={y}$
104 fveqeq2 ${⊢}{w}={v}\setminus \left\{{n}\right\}\to \left(\left|{w}\right|={y}↔\left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
105 103 104 syl5bb ${⊢}{w}={v}\setminus \left\{{n}\right\}\to \left({y}=\left|{w}\right|↔\left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
106 105 adantr ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({y}=\left|{w}\right|↔\left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
107 102 106 anbi12d
108 107 6 imbi12d
109 108 spc2gv
110 98 1 109 mp2an
111 110 expdimp
113 73 3anbi2i
114 113 anbi2i
115 114 8 sylanb
116 97 112 115 syl6an
117 116 exp41
118 117 com15
119 118 com23
120 88 119 mpcom
121 120 ex
122 121 com23
123 122 ex
124 123 com15
125 124 imp
126 5 125 mpd
127 126 ex
128 127 com4l
129 128 exlimiv
130 80 129 syl
131 130 ex
132 131 com25
133 132 elv
134 133 imp
135 134 impcom
136 79 135 mpd
137 72 136 sylan
138 137 impancom
139 138 alrimivv
140 139 ex
141 48 140 syl5bi
142 22 26 30 34 38 141 uzind
143 11 13 18 142 syl3anc
144 sbcex
145 sbccom
146 sbcex
147 145 146 sylbi
148 144 147 jca
149 simpl ${⊢}\left({v}={V}\wedge {e}={E}\right)\to {v}={V}$
150 simpr ${⊢}\left({v}={V}\wedge {e}={E}\right)\to {e}={E}$
151 150 sbceq1d
152 149 151 sbceqbid
153 fveq2 ${⊢}{v}={V}\to \left|{v}\right|=\left|{V}\right|$
154 153 eqeq2d ${⊢}{v}={V}\to \left({n}=\left|{v}\right|↔{n}=\left|{V}\right|\right)$
155 154 adantr ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({n}=\left|{v}\right|↔{n}=\left|{V}\right|\right)$
156 152 155 anbi12d
157 156 3 imbi12d
158 157 spc2gv
159 158 com23
160 159 expd
161 148 160 mpcom
162 161 imp
163 143 162 syl5com
164 163 exp31
165 164 com14
166 165 expcom
167 166 com24
168 167 pm2.43i
169 168 imp
170 169 exlimiv
171 9 170 sylbi
172 hashcl ${⊢}{V}\in \mathrm{Fin}\to \left|{V}\right|\in {ℕ}_{0}$
173 171 172 syl11
174 173 3imp