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		ffvelrn	$⊢ (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		ffvelrn	$⊢ (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	biimpi	$⊢ I (F (0)) = \{P (0), P (1)\} \to I (F (0)) = \{P (1), P (0)\}$
24	23	adantr	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (0)) = \{P (1), P (0)\}$
25	24	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)\}$
26	2	usgrnloopv	$⊢ (G \in USGraph \land P (1) \in V) \to (I (F (0)) = \{P (1), P (0)\} \to P (1) \neq P (0))$
27	20 25 26	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)$
28	27	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)$
29	19	elsn	$⊢ P (1) \in \{P (0)\} \leftrightarrow P (1) = P (0)$
30	29	necon3bbii	$⊢ \neg P (1) \in \{P (0)\} \leftrightarrow P (1) \neq P (0)$
31	28 30	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)\}$
32	17 31	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)\})$
33	32	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)\})$
34		sneq	$⊢ x = P (0) \to \{x\} = \{P (0)\}$
35	34	difeq2d	$⊢ x = P (0) \to V ∖ \{x\} = V ∖ \{P (0)\}$
36	35	eleq2d	$⊢ x = P (0) \to (P (1) \in (V ∖ \{x\}) \leftrightarrow P (1) \in (V ∖ \{P (0)\}))$
37	36	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)\}))$
38	33 37	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\})$
39		2re	$⊢ 2 \in ℝ$
40	39	leidi	$⊢ 2 \leq 2$
41		elfz2nn0	$⊢ 2 \in (0 \dots 2) \leftrightarrow (2 \in ℕ_{0} \land 2 \in ℕ_{0} \land 2 \leq 2)$
42	4 4 40 41	mpbir3an	$⊢ 2 \in (0 \dots 2)$
43		ffvelrn	$⊢ (P : (0 \dots 2) ⟶ V \land 2 \in (0 \dots 2)) \to P (2) \in V$
44	42 43	mpan2	$⊢ P : (0 \dots 2) ⟶ V \to P (2) \in V$
45	44	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$
46	2	usgrf1	$⊢ G \in USGraph \to I : dom I \underset{1-1}{⟶} ran I$
47	46	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$
48		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$
49	48	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$
50	47 49	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)$
51		2nn	$⊢ 2 \in ℕ$
52		lbfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow 2 \in ℕ$
53	51 52	mpbir	$⊢ 0 \in (0 ..^2)$
54		1lt2	$⊢ 1 < 2$
55		elfzo0	$⊢ 1 \in (0 ..^2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ \land 1 < 2)$
56	11 51 54 55	mpbir3an	$⊢ 1 \in (0 ..^2)$
57	53 56	pm3.2i	$⊢ (0 \in (0 ..^2) \land 1 \in (0 ..^2))$
58	57	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))$
59		0ne1	$⊢ 0 \neq 1$
60	59	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$
61	50 58 60	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)$
62		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)\})$
63	62	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)\})$
64		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)\})$
65	61 63 64	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)\}$
66		necom	$⊢ P (2) \neq P (0) \leftrightarrow P (0) \neq P (2)$
67		fvex	$⊢ P (0) \in V$
68		fvex	$⊢ P (2) \in V$
69	67 19 68	3pm3.2i	$⊢ (P (0) \in V \land P (1) \in V \land P (2) \in V)$
70		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$
71		simpl	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (0)) = \{P (0), P (1)\}$
72	71	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)\}$
73	18 70 72	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)\})$
74	73	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)\})$
75	2	usgrnloopv	$⊢ (G \in USGraph \land P (0) \in V) \to (I (F (0)) = \{P (0), P (1)\} \to P (0) \neq P (1))$
76	75	imp	$⊢ ((G \in USGraph \land P (0) \in V) \land I (F (0)) = \{P (0), P (1)\}) \to P (0) \neq P (1)$
77	74 76	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)$
78		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)\})$
79	69 77 78	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)\})$
80	66 79	syl5bb	$⊢ (((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)\})$
81	65 80	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)$
82		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$
83		prcom	$⊢ \{P (1), P (2)\} = \{P (2), P (1)\}$
84	83	eqeq2i	$⊢ I (F (1)) = \{P (1), P (2)\} \leftrightarrow I (F (1)) = \{P (2), P (1)\}$
85	84	biimpi	$⊢ I (F (1)) = \{P (1), P (2)\} \to I (F (1)) = \{P (2), P (1)\}$
86	85	adantl	$⊢ (I (F (0)) = \{P (0), P (1)\} \land I (F (1)) = \{P (1), P (2)\}) \to I (F (1)) = \{P (2), P (1)\}$
87	86	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)\}$
88	18 82 87	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)\})$
89	88	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)\})$
90	2	usgrnloopv	$⊢ (G \in USGraph \land P (2) \in V) \to (I (F (1)) = \{P (2), P (1)\} \to P (2) \neq P (1))$
91	90	imp	$⊢ ((G \in USGraph \land P (2) \in V) \land I (F (1)) = \{P (2), P (1)\}) \to P (2) \neq P (1)$
92	89 91	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)$
93	81 92	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)\}$
94	45 93	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)\})$
95	94	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)\})$
96		preq12	$⊢ (x = P (0) \land y = P (1)) \to \{x, y\} = \{P (0), P (1)\}$
97	96	difeq2d	$⊢ (x = P (0) \land y = P (1)) \to V ∖ \{x, y\} = V ∖ \{P (0), P (1)\}$
98	97	eleq2d	$⊢ (x = P (0) \land y = P (1)) \to (P (2) \in (V ∖ \{x, y\}) \leftrightarrow P (2) \in (V ∖ \{P (0), P (1)\}))$
99	98	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)\}))$
100	95 99	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\})$
101		eqcom	$⊢ x = P (0) \leftrightarrow P (0) = x$
102		eqcom	$⊢ y = P (1) \leftrightarrow P (1) = y$
103		eqcom	$⊢ z = P (2) \leftrightarrow P (2) = z$
104	101 102 103	3anbi123i	$⊢ (x = P (0) \land y = P (1) \land z = P (2)) \leftrightarrow (P (0) = x \land P (1) = y \land P (2) = z)$
105	104	biimpi	$⊢ (x = P (0) \land y = P (1) \land z = P (2)) \to (P (0) = x \land P (1) = y \land P (2) = z)$
106	105	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)$
107	101	biimpi	$⊢ x = P (0) \to P (0) = x$
108	107	ad2antrr	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (0) = x$
109	102	biimpi	$⊢ y = P (1) \to P (1) = y$
110	109	ad2antlr	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (1) = y$
111	108 110	preq12d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to \{P (0), P (1)\} = \{x, y\}$
112	111	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\})$
113	103	biimpi	$⊢ z = P (2) \to P (2) = z$
114	113	adantl	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to P (2) = z$
115	110 114	preq12d	$⊢ ((x = P (0) \land y = P (1)) \land z = P (2)) \to \{P (1), P (2)\} = \{y, z\}$
116	115	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\})$
117	112 116	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\}))$
118	117	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\})$
119	106 118	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\}))$
120	119	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\})))))$
121	120	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\})))))$
122	121	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\})))$
123	100 122	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\})))$
124	38 123	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\})))$
125	10 124	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\})))$
126	125	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\}))))))$
127	126	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\}))))))$
128	127	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\})))))$
129	128	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\})))))$
130	129	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\})))))$
131		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
132	131	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)\})$
133		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
134	133	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)\}$
135		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)\})$
136	134 135	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)\})$
137	132 136	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)\}))$
138	137	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)\}))$
139		oveq2	$⊢ \|F\| = 2 \to (0 \dots \|F\|) = (0 \dots 2)$
140	139	feq2d	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
141	140	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to (P : (0 \dots \|F\|) ⟶ V \leftrightarrow P : (0 \dots 2) ⟶ V)$
142		f1eq2	$⊢ (0 ..^\|F\|) = (0 ..^2) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
143	131 142	syl	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow F : (0 ..^2) \underset{1-1}{⟶} dom I)$
144	143	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\}))))$
145	144	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\}))))$
146	141 145	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\})))))$
147	130 138 146	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\})))))$
148	147	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\})))))$
149	148	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\})))))$
150	149	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