konigsberglem4 - Intuitionistic Logic Explorer

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

Theorem konigsberglem4 16486

Description: Lemma 4 for konigsberg 16488: 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 9514	. . . . . 6 ⊢ 3 ∈ ℕ₀
2		0elfz 10452	. . . . . 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 2308	. . . 4 ⊢ 0 ∈ 𝑉
6		n2dvds3 12601	. . . . 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 16483	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘0) = 3
10	9	breq2i 4117	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘0) ↔ 2 ∥ 3)
11	6, 10	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)
12		fveq2 5670	. . . . . . 7 ⊢ (𝑥 = 0 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘0))
13	12	breq2d 4121	. . . . . 6 ⊢ (𝑥 = 0 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘0)))
14	13	notbid 673	. . . . 5 ⊢ (𝑥 = 0 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)))
15	14	elrab 2973	. . . 4 ⊢ (0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ↔ (0 ∈ 𝑉 ∧ ¬ 2 ∥ ((VtxDeg‘𝐺)‘0)))
16	5, 11, 15	mpbir2an 951	. . 3 ⊢ 0 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
17		1nn0 9512	. . . . . 6 ⊢ 1 ∈ ℕ₀
18		1le3 9449	. . . . . 6 ⊢ 1 ≤ 3
19		elfz2nn0 10446	. . . . . 6 ⊢ (1 ∈ (0...3) ↔ (1 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 1 ≤ 3))
20	17, 1, 18, 19	mpbir3an 1206	. . . . 5 ⊢ 1 ∈ (0...3)
21	20, 4	eleqtrri 2308	. . . 4 ⊢ 1 ∈ 𝑉
22	4, 7, 8	konigsberglem2 16484	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘1) = 3
23	22	breq2i 4117	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘1) ↔ 2 ∥ 3)
24	6, 23	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)
25		fveq2 5670	. . . . . . 7 ⊢ (𝑥 = 1 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘1))
26	25	breq2d 4121	. . . . . 6 ⊢ (𝑥 = 1 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘1)))
27	26	notbid 673	. . . . 5 ⊢ (𝑥 = 1 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)))
28	27	elrab 2973	. . . 4 ⊢ (1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} ↔ (1 ∈ 𝑉 ∧ ¬ 2 ∥ ((VtxDeg‘𝐺)‘1)))
29	21, 24, 28	mpbir2an 951	. . 3 ⊢ 1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
30		3re 9311	. . . . . . 7 ⊢ 3 ∈ ℝ
31	30	leidi 8759	. . . . . 6 ⊢ 3 ≤ 3
32		elfz2nn0 10446	. . . . . 6 ⊢ (3 ∈ (0...3) ↔ (3 ∈ ℕ₀ ∧ 3 ∈ ℕ₀ ∧ 3 ≤ 3))
33	1, 1, 31, 32	mpbir3an 1206	. . . . 5 ⊢ 3 ∈ (0...3)
34	33, 4	eleqtrri 2308	. . . 4 ⊢ 3 ∈ 𝑉
35	4, 7, 8	konigsberglem3 16485	. . . . . 6 ⊢ ((VtxDeg‘𝐺)‘3) = 3
36	35	breq2i 4117	. . . . 5 ⊢ (2 ∥ ((VtxDeg‘𝐺)‘3) ↔ 2 ∥ 3)
37	6, 36	mtbir 678	. . . 4 ⊢ ¬ 2 ∥ ((VtxDeg‘𝐺)‘3)
38		fveq2 5670	. . . . . . 7 ⊢ (𝑥 = 3 → ((VtxDeg‘𝐺)‘𝑥) = ((VtxDeg‘𝐺)‘3))
39	38	breq2d 4121	. . . . . 6 ⊢ (𝑥 = 3 → (2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ 2 ∥ ((VtxDeg‘𝐺)‘3)))
40	39	notbid 673	. . . . 5 ⊢ (𝑥 = 3 → (¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥) ↔ ¬ 2 ∥ ((VtxDeg‘𝐺)‘3)))
41	40	elrab 2973	. . . 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 8268	. . 3 ⊢ 0 ∈ V
45		1ex 8269	. . 3 ⊢ 1 ∈ V
46		3ex 9313	. . 3 ⊢ 3 ∈ V
47	44, 45, 46	tpss 3862	. 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 2203 {crab 2524 ⊆ wss 3211 {cpr 3690 {ctp 3691 ⟨cop 3692 class class class wbr 4109 ‘cfv 5352 (class class class)co 6050 0cc0 8127 1c1 8128 ≤ cle 8309 2c2 9288 3c3 9289 ℕ₀cn0 9496 ...cfz 10342 ⟨“cs7 11446 ∥ cdvds 12473 VtxDegcvtxdg 16281

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 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-iinf 4710 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-mulrcl 8226 ax-addcom 8227 ax-mulcom 8228 ax-addass 8229 ax-mulass 8230 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-1rid 8234 ax-0id 8235 ax-rnegex 8236 ax-precex 8237 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-apti 8242 ax-pre-ltadd 8243 ax-pre-mulgt0 8244 ax-pre-mulext 8245

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 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-if 3621 df-pw 3671 df-sn 3695 df-pr 3696 df-tp 3697 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-po 4417 df-iso 4418 df-iord 4487 df-on 4489 df-ilim 4490 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-recs 6536 df-irdg 6601 df-frec 6622 df-1o 6647 df-2o 6648 df-oadd 6651 df-er 6767 df-en 6976 df-dom 6977 df-fin 6978 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-reap 8849 df-ap 8856 df-div 8947 df-inn 9238 df-2 9296 df-3 9297 df-4 9298 df-5 9299 df-6 9300 df-7 9301 df-8 9302 df-9 9303 df-n0 9497 df-z 9578 df-dec 9710 df-uz 9854 df-xadd 10106 df-fz 10343 df-fzo 10477 df-ihash 11139 df-word 11225 df-concat 11279 df-s1 11304 df-s2 11448 df-s3 11449 df-s4 11450 df-s5 11451 df-s6 11452 df-s7 11453 df-dvds 12474 df-ndx 13215 df-slot 13216 df-base 13218 df-edgf 16000 df-vtx 16009 df-iedg 16010 df-upgren 16088 df-umgren 16089 df-vtxdg 16282

This theorem is referenced by: konigsberglem5 16487

W3C validator