usgr2pthlem

	Ref	Expression
Hypotheses	usgr2pthlem.v	$⊢ V = Vtx (G)$
	usgr2pthlem.i	$⊢ I = iEdg (G)$
Assertion	usgr2pthlem	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$

Proof

Step	Hyp	Ref	Expression
1		usgr2pthlem.v	$⊢ V = Vtx (G)$
2		usgr2pthlem.i	$⊢ I = iEdg (G)$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5		0le2	$⊢ 0 \leq 2$
6		elfz2nn0	$⊢ 0 \in (0 \dots 2) \leftrightarrow (0 \in ℕ_{0} \land 2 \in ℕ_{0} \land 0 \leq 2)$
7	3 4 5 6	mpbir3an	$⊢ 0 \in (0 \dots 2)$
8		ffvelcdm	$⊢ (P : (0 \dots 2) ⟶ V \land 0 \in (0 \dots 2)) \to P (0) \in V$
9	7 8	mpan2	$⊢ P : (0 \dots 2) ⟶ V \to P (0) \in V$
10	9	adantl	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (0) \in V$
11		1nn0	$⊢ 1 \in ℕ_{0}$
12		1le2	$⊢ 1 \leq 2$
13		elfz2nn0	$⊢ 1 \in (0 \dots 2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ_{0} \land 1 \leq 2)$
14	11 4 12 13	mpbir3an	$⊢ 1 \in (0 \dots 2)$
15		ffvelcdm	$⊢ (P : (0 \dots 2) ⟶ V \land 1 \in (0 \dots 2)) \to P (1) \in V$
16	14 15	mpan2	$⊢ P : (0 \dots 2) ⟶ V \to P (1) \in V$
17	16	adantl	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (1) \in V$
18		simpr	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to G \in USGraph$
19		fvex	$⊢ P (1) \in V$
20	18 19	jctir	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to (G \in USGraph \land P (1) \in V)$
21		prcom	$⊢ \{P (0), P (1)\} = \{P (1), P (0)\}$
22	21	eqeq2i	$⊢ I (F (0)) = \{P (0), P (1)\} \leftrightarrow I (F (0)) = \{P (1), P (0)\}$
23	22	birani	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (0)) = \{P (1), P (0)\}$
24	23	ad2antlr	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to I (F (0)) = \{P (1), P (0)\}$
25	2	usgrnloopv	$⊢ (G \in USGraph \land P (1) \in V) \to (I (F (0)) = \{P (1), P (0)\} \to P (1) \neq P (0))$
26	20 24 25	sylc	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to P (1) \neq P (0)$
27	26	adantr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (1) \neq P (0)$
28	19	elsn	$⊢ P (1) \in \{P (0)\} \leftrightarrow P (1) = P (0)$
29	28	necon3bbii	$⊢ \neg P (1) \in \{P (0)\} \leftrightarrow P (1) \neq P (0)$
30	27 29	sylibr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to \neg P (1) \in \{P (0)\}$
31	17 30	eldifd	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (1) \in (V ∖ \{P (0)\})$
32	31	adantr	$⊢ ((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \to P (1) \in (V ∖ \{P (0)\})$
33		sneq	$⊢ x = P (0) \to \{x\} = \{P (0)\}$
34	33	difeq2d	$⊢ x = P (0) \to V ∖ \{x\} = V ∖ \{P (0)\}$
35	34	eleq2d	$⊢ x = P (0) \to (P (1) \in (V ∖ \{x\}) \leftrightarrow P (1) \in (V ∖ \{P (0)\}))$
36	35	adantl	$⊢ ((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \to (P (1) \in (V ∖ \{x\}) \leftrightarrow P (1) \in (V ∖ \{P (0)\}))$
37	32 36	mpbird	$⊢ ((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \to P (1) \in (V ∖ \{x\})$
38		2re	$⊢ 2 \in ℝ$
39	38	leidi	$⊢ 2 \leq 2$
40		elfz2nn0	$⊢ 2 \in (0 \dots 2) \leftrightarrow (2 \in ℕ_{0} \land 2 \in ℕ_{0} \land 2 \leq 2)$
41	4 4 39 40	mpbir3an	$⊢ 2 \in (0 \dots 2)$
42		ffvelcdm	$⊢ (P : (0 \dots 2) ⟶ V \land 2 \in (0 \dots 2)) \to P (2) \in V$
43	41 42	mpan2	$⊢ P : (0 \dots 2) ⟶ V \to P (2) \in V$
44	43	adantl	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (2) \in V$
45	2	usgrf1	$⊢ G \in USGraph \to I : dom I \underset{1-1}{⟶} ran I$
46	45	ad2antlr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to I : dom I \underset{1-1}{⟶} ran I$
47		simpl	$⊢ (F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \to F : (0 ..^2) \underset{1-1}{⟶} dom I$
48	47	ad2antrr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to F : (0 ..^2) \underset{1-1}{⟶} dom I$
49	46 48	jca	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to (I : dom I \underset{1-1}{⟶} ran I \land F : (0 ..^2) \underset{1-1}{⟶} dom I)$
50		2nn	$⊢ 2 \in ℕ$
51		lbfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow 2 \in ℕ$
52	50 51	mpbir	$⊢ 0 \in (0 ..^2)$
53		1lt2	$⊢ 1 < 2$
54		elfzo0	$⊢ 1 \in (0 ..^2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ \land 1 < 2)$
55	11 50 53 54	mpbir3an	$⊢ 1 \in (0 ..^2)$
56	52 55	pm3.2i	$⊢ (0 \in (0 ..^2) \land 1 \in (0 ..^2))$
57	56	a1i	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to (0 \in (0 ..^2) \land 1 \in (0 ..^2))$
58		0ne1	$⊢ 0 \neq 1$
59	58	a1i	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to 0 \neq 1$
60	49 57 59	3jca	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to ((I : dom I \underset{1-1}{⟶} ran I \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land (0 \in (0 ..^2) \land 1 \in (0 ..^2)) \land 0 \neq 1)$
61		simpr	$⊢ (F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
62	61	ad2antrr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
63		2f1fvneq	$⊢ ((I : dom I \underset{1-1}{⟶} ran I \land F : (0 ..^2) \underset{1-1}{⟶} dom I) \land (0 \in (0 ..^2) \land 1 \in (0 ..^2)) \land 0 \neq 1) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to \{P (0), P (1)\} \neq \{P (1), P (2)\})$
64	60 62 63	sylc	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to \{P (0), P (1)\} \neq \{P (1), P (2)\}$
65		necom	$⊢ P (2) \neq P (0) \leftrightarrow P (0) \neq P (2)$
66		fvex	$⊢ P (0) \in V$
67		fvex	$⊢ P (2) \in V$
68	66 19 67	3pm3.2i	$⊢ (P (0) \in V \land P (1) \in V \land P (2) \in V)$
69		fvexd	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to P (0) \in V$
70		simpl	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (0)) = \{P (0), P (1)\}$
71	70	ad2antlr	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to I (F (0)) = \{P (0), P (1)\}$
72	18 69 71	jca31	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to ((G \in USGraph \land P (0) \in V) \land I (F (0)) = \{P (0), P (1)\})$
73	72	adantr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to ((G \in USGraph \land P (0) \in V) \land I (F (0)) = \{P (0), P (1)\})$
74	2	usgrnloopv	$⊢ (G \in USGraph \land P (0) \in V) \to (I (F (0)) = \{P (0), P (1)\} \to P (0) \neq P (1))$
75	74	imp	$⊢ ((G \in USGraph \land P (0) \in V) \land I (F (0)) = \{P (0), P (1)\}) \to P (0) \neq P (1)$
76	73 75	syl	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (0) \neq P (1)$
77		pr1nebg	$⊢ ((P (0) \in V \land P (1) \in V \land P (2) \in V) \land P (0) \neq P (1)) \to (P (0) \neq P (2) \leftrightarrow \{P (0), P (1)\} \neq \{P (1), P (2)\})$
78	68 76 77	sylancr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to (P (0) \neq P (2) \leftrightarrow \{P (0), P (1)\} \neq \{P (1), P (2)\})$
79	65 78	bitrid	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to (P (2) \neq P (0) \leftrightarrow \{P (0), P (1)\} \neq \{P (1), P (2)\})$
80	64 79	mpbird	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (2) \neq P (0)$
81		fvexd	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to P (2) \in V$
82		prcom	$⊢ \{P (1), P (2)\} = \{P (2), P (1)\}$
83	82	eqeq2i	$⊢ I (F (1)) = \{P (1), P (2)\} \leftrightarrow I (F (1)) = \{P (2), P (1)\}$
84	83	bilani	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (1)) = \{P (2), P (1)\}$
85	84	ad2antlr	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to I (F (1)) = \{P (2), P (1)\}$
86	18 81 85	jca31	$⊢ ((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \to ((G \in USGraph \land P (2) \in V) \land I (F (1)) = \{P (2), P (1)\})$
87	86	adantr	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to ((G \in USGraph \land P (2) \in V) \land I (F (1)) = \{P (2), P (1)\})$
88	2	usgrnloopv	$⊢ (G \in USGraph \land P (2) \in V) \to (I (F (1)) = \{P (2), P (1)\} \to P (2) \neq P (1))$
89	88	imp	$⊢ ((G \in USGraph \land P (2) \in V) \land I (F (1)) = \{P (2), P (1)\}) \to P (2) \neq P (1)$
90	87 89	syl	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (2) \neq P (1)$
91	80 90	nelprd	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to \neg P (2) \in \{P (0), P (1)\}$
92	44 91	eldifd	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to P (2) \in (V ∖ \{P (0), P (1)\})$
93	92	ad2antrr	$⊢ (((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \land y = P (1)) \to P (2) \in (V ∖ \{P (0), P (1)\})$
94		preq12	$⊢ (x = P (0) \land y = P (1)) \to \{x, y\} = \{P (0), P (1)\}$
95	94	difeq2d	$⊢ (x = P (0) \land y = P (1)) \to V ∖ \{x, y\} = V ∖ \{P (0), P (1)\}$
96	95	eleq2d	$⊢ (x = P (0) \land y = P (1)) \to (P (2) \in (V ∖ \{x, y\}) \leftrightarrow P (2) \in (V ∖ \{P (0), P (1)\}))$
97	96	adantll	$⊢ (((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \land y = P (1)) \to (P (2) \in (V ∖ \{x, y\}) \leftrightarrow P (2) \in (V ∖ \{P (0), P (1)\}))$
98	93 97	mpbird	$⊢ (((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \land y = P (1)) \to P (2) \in (V ∖ \{x, y\})$
99		eqcom	$⊢ x = P (0) \leftrightarrow P (0) = x$
100		eqcom	$⊢ y = P (1) \leftrightarrow P (1) = y$
101		eqcom	$⊢ z = P (2) \leftrightarrow P (2) = z$
102	99 100 101	3anbi123i	$⊢ (x = P (0) \land y = P (1) \land z = P (2)) \leftrightarrow (P (0) = x \land P (1) = y \land P (2) = z)$
103	102	biimpi	$⊢ (x = P (0) \land y = P (1) \land z = P (2)) \to (P (0) = x \land P (1) = y \land P (2) = z)$
104	103	ad4ant123	$⊢ (((x = P (0) \land y = P (1)) \land z = P (2)) \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \to (P (0) = x \land P (1) = y \land P (2) = z)$
105	99	biimpi	$⊢ x = P (0) \to P (0) = x$
106	105	ad2antrr	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (0) = x$
107	100	biimpi	$⊢ y = P (1) \to P (1) = y$
108	107	ad2antlr	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (1) = y$
109	106 108	preq12d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to \{P (0), P (1)\} = \{x, y\}$
110	109	eqeq2d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to (I (F (0)) = \{P (0), P (1)\} \leftrightarrow I (F (0)) = \{x, y\})$
111	101	bilani	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (2) = z$
112	108 111	preq12d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to \{P (1), P (2)\} = \{y, z\}$
113	112	eqeq2d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to (I (F (1)) = \{P (1), P (2)\} \leftrightarrow I (F (1)) = \{y, z\})$
114	110 113	anbi12d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \leftrightarrow (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))$
115	114	biimpa	$⊢ (((x = P (0) \land y = P (1)) \land z = P (2)) \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \to (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})$
116	104 115	jca	$⊢ (((x = P (0) \land y = P (1)) \land z = P (2)) \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \to ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))$
117	116	exp41	$⊢ x = P (0) \to (y = P (1) \to (z = P (2) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
118	117	adantl	$⊢ ((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \to (y = P (1) \to (z = P (2) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
119	118	imp31	$⊢ ((((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \land y = P (1)) \land z = P (2)) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
120	98 119	rspcimedv	$⊢ (((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \land y = P (1)) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
121	37 120	rspcimedv	$⊢ ((((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \land x = P (0)) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
122	10 121	rspcimedv	$⊢ (((F : (0 ..^2) \underset{1-1}{⟶} dom I \land (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})) \land G \in USGraph) \land P : (0 \dots 2) ⟶ V) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$
123	122	exp41	$⊢ F : (0 ..^2) \underset{1-1}{⟶} dom I \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to (G \in USGraph \to (P : (0 \dots 2) ⟶ V \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))))$
124	123	com15	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to (G \in USGraph \to (P : (0 \dots 2) ⟶ V \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))))$
125	124	pm2.43i	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to (G \in USGraph \to (P : (0 \dots 2) ⟶ V \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
126	125	com12	$⊢ G \in USGraph \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to (P : (0 \dots 2) ⟶ V \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
127	126	adantr	$⊢ (G \in USGraph \land \|F\| = 2) \to ((I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to (P : (0 \dots 2) ⟶ V \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
128		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
129	128	raleqdv	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow \forall i \in (0 ..^2) I (F (i)) = \{P (i), P (i + 1)\})$
130		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
131	130	raleqi	$⊢ \forall i \in (0 ..^2) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow \forall i \in \{0, 1\} I (F (i)) = \{P (i), P (i + 1)\}$
132		2wlklem	$⊢ \forall i \in \{0, 1\} I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
133	131 132	bitri	$⊢ \forall i \in (0 ..^2) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\})$
134	129 133	bitrdi	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))$
135	134	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}))$
136		oveq2	$⊢ \|F\| = 2 \to (0 \dots \|F\|) = (0 \dots 2)$
137	136	feq2d	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
138	137	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
139		f1eq2	$⊢ (0 ..^\|F\|) = (0 ..^2) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
140	128 139	syl	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
141	140	imbi1d	$⊢ \|F\| = 2 \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
142	141	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))) \leftrightarrow (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\}))))$
143	138 142	imbi12d	$⊢ (G \in USGraph \land \|F\| = 2) \to ((P : (0 \dots \|F\|) ⟶ V \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))) \leftrightarrow (P : (0 \dots 2) ⟶ V \to (F : (0 ..^2) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
144	127 135 143	3imtr4d	$⊢ (G \in USGraph \land \|F\| = 2) \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \to (P : (0 \dots \|F\|) ⟶ V \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
145	144	com14	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \to (P : (0 \dots \|F\|) ⟶ V \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
146	145	com23	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to (P : (0 \dots \|F\|) ⟶ V \to (\forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\} \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))))$
147	146	3imp	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) I (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to \exists x \in V \exists y \in (V ∖ \{x\}) \exists z \in (V ∖ \{x, y\}) ((P (0) = x \land P (1) = y \land P (2) = z) \land (I (F (0)) = \{x, y\} \land I (F (1)) = \{y, z\})))$

Metamath Proof Explorer

Theorem usgr2pthlem

Proof