konigsberglem4 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > konigsberglem4		GIF version

Theorem konigsberglem4 16415

Description: Lemma 4 for konigsberg 16417: Vertices 0, 1, 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.)

**Hypotheses**
Ref	Expression
konigsberg.v	⊢ 𝑉 = (0...3)
konigsberg.e	⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩
konigsberg.g	⊢ 𝐺 = ⟨𝑉, 𝐸⟩

**Assertion**
Ref	Expression
konigsberglem4	⊢ {0, 1, 3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}

Distinct variable groups: 𝑥,𝑉 𝑥,𝐺 Allowed substitution hint: 𝐸(𝑥)

**Proof of Theorem konigsberglem4**
Step	Hyp	Ref	Expression
1		3nn0 9462	. . . . . 6 ⊢ 3 ∈ ℕ₀
2		0elfz 10398	. . . . . 6 ⊢ (3 ∈ ℕ₀ → 0 ∈ (0...3))
3	1, 2	ax-mp 5	. . . . 5 ⊢ 0 ∈ (0...3)
4		konigsberg.v	. . . . 5 ⊢ 𝑉 = (0...3)
5	3, 4	eleqtrri 2307	. . . 4 ⊢ 0 ∈ 𝑉
6		n2dvds3 12539	. . . . 5 ⊢ ¬ 2 ∥ 3
7		konigsberg.e	. . . . . . 7 ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩
8		konigsberg.g	. . . . . . 7 ⊢ 𝐺 = ⟨𝑉, 𝐸⟩
9	4, 7, 8	konigsberglem1 16412	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘0) = 3
10	9	breq2i 4101	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘0) ↔ 2 ∥ 3)
11	6, 10	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)
12		fveq2 5648	. . . . . . 7 ⊢ (𝑥 = 0 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘0))
13	12	breq2d 4105	. . . . . 6 ⊢ (𝑥 = 0 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘0)))
14	13	notbid 673	. . . . 5 ⊢ (𝑥 = 0 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)))
15	14	elrab 2963	. . . 4 ⊢ (0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ↔ (0 ∈ 𝑉 ∧ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)))
16	5, 11, 15	mpbir2an 951	. . 3 ⊢ 0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
17		1nn0 9460	. . . . . 6 ⊢ 1 ∈ ℕ₀
18		1le3 9397	. . . . . 6 ⊢ 1 ≤ 3
19		elfz2nn0 10392	. . . . . 6 ⊢ (1 ∈ (0...3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 1 ≤ 3))
20	17, 1, 18, 19	mpbir3an 1206	. . . . 5 ⊢ 1 ∈ (0...3)
21	20, 4	eleqtrri 2307	. . . 4 ⊢ 1 ∈ 𝑉
22	4, 7, 8	konigsberglem2 16413	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘1) = 3
23	22	breq2i 4101	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘1) ↔ 2 ∥ 3)
24	6, 23	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)
25		fveq2 5648	. . . . . . 7 ⊢ (𝑥 = 1 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘1))
26	25	breq2d 4105	. . . . . 6 ⊢ (𝑥 = 1 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘1)))
27	26	notbid 673	. . . . 5 ⊢ (𝑥 = 1 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)))
28	27	elrab 2963	. . . 4 ⊢ (1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ↔ (1 ∈ 𝑉 ∧ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)))
29	21, 24, 28	mpbir2an 951	. . 3 ⊢ 1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
30		3re 9259	. . . . . . 7 ⊢ 3 ∈ ℝ
31	30	leidi 8707	. . . . . 6 ⊢ 3 ≤ 3
32		elfz2nn0 10392	. . . . . 6 ⊢ (3 ∈ (0...3) ↔ (3 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 ≤ 3))
33	1, 1, 31, 32	mpbir3an 1206	. . . . 5 ⊢ 3 ∈ (0...3)
34	33, 4	eleqtrri 2307	. . . 4 ⊢ 3 ∈ 𝑉
35	4, 7, 8	konigsberglem3 16414	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘3) = 3
36	35	breq2i 4101	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘3) ↔ 2 ∥ 3)
37	6, 36	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘3)
38		fveq2 5648	. . . . . . 7 ⊢ (𝑥 = 3 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘3))
39	38	breq2d 4105	. . . . . 6 ⊢ (𝑥 = 3 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘3)))
40	39	notbid 673	. . . . 5 ⊢ (𝑥 = 3 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘3)))
41	40	elrab 2963	. . . 4 ⊢ (3 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ↔ (3 ∈ 𝑉 ∧ ¬ 2 ∥ ((VtxDeg‘𝐺)‘3)))
42	34, 37, 41	mpbir2an 951	. . 3 ⊢ 3 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
43	16, 29, 42	3pm3.2i 1202	. 2 ⊢ (0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ∧ 1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ∧ 3 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)})
44		c0ex 8216	. . 3 ⊢ 0 ∈ V
45		1ex 8217	. . 3 ⊢ 1 ∈ V
46		3ex 9261	. . 3 ⊢ 3 ∈ V
47	44, 45, 46	tpss 3846	. 2 ⊢ ((0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ∧ 1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ∧ 3 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) ↔ {0, 1, 3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)})
48	43, 47	mpbi 145	1 ⊢ {0, 1, 3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}

Colors of variables: wff set class

Syntax hints: ¬ wn 3 ∧ w3a 1005 = wceq 1398 ∈ wcel 2202 {crab 2515 ⊆ wss 3201 {cpr 3674 {ctp 3675 ⟨cop 3676 class class class wbr 4093 ‘cfv 5333 (class class class)co 6028 0cc0 8075 1c1 8076 ≤ cle 8257 2c2 9236 3c3 9237 ℕ₀cn0 9444 ...cfz 10288 ⟨“cs7 11384 ∥ cdvds 12411 VtxDegcvtxdg 16210

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-xor 1421 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-tp 3681 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-frec 6600 df-1o 6625 df-2o 6626 df-oadd 6629 df-er 6745 df-en 6953 df-dom 6954 df-fin 6955 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-3 9245 df-4 9246 df-5 9247 df-6 9248 df-7 9249 df-8 9250 df-9 9251 df-n0 9445 df-z 9524 df-dec 9656 df-uz 9800 df-xadd 10052 df-fz 10289 df-fzo 10423 df-ihash 11084 df-word 11163 df-concat 11217 df-s1 11242 df-s2 11386 df-s3 11387 df-s4 11388 df-s5 11389 df-s6 11390 df-s7 11391 df-dvds 12412 df-ndx 13148 df-slot 13149 df-base 13151 df-edgf 15929 df-vtx 15938 df-iedg 15939 df-upgren 16017 df-umgren 16018 df-vtxdg 16211

This theorem is referenced by: konigsberglem5 16416

W3C validator