usgr2pthlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > usgr2pthlem		Structured version Visualization version GIF version

Theorem usgr2pthlem 30112

Description: Lemma for usgr2pth 30113. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)

**Hypotheses**
Ref	Expression
usgr2pthlem.v	⊢ 𝑉 = (Vtx‘𝐺)
usgr2pthlem.i	⊢ 𝐼 = (iEdg‘𝐺)

**Assertion**
Ref	Expression
usgr2pthlem	⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))

Distinct variable groups: 𝑖,𝐹 𝑥,𝐹,𝑦,𝑧 𝑥,𝐺,𝑦,𝑧 𝑖,𝐼 𝑥,𝐼,𝑦,𝑧 𝑃,𝑖 𝑥,𝑃,𝑦,𝑧 𝑥,𝑉,𝑦,𝑧 Allowed substitution hints: 𝐺(𝑖) 𝑉(𝑖)

**Proof of Theorem usgr2pthlem**
Step	Hyp	Ref	Expression
1		0nn0 12514	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ₀
2		2nn0 12516	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ₀
3		0le2 12338	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
4		elfz2nn0 13642	. . . . . . . . . . . . . 14 ⊢ (0 ∈ (0...2) ↔ (0 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 0 ≤ 2))
5	1, 2, 3, 4	mpbir3an 1360	. . . . . . . . . . . . 13 ⊢ 0 ∈ (0...2)
6		ffvelcdm 7076	. . . . . . . . . . . . 13 ⊢ ((𝑃:(0...2)⟶𝑉 ∧ 0 ∈ (0...2)) → (𝑃‘0) ∈ 𝑉)
7	5, 6	mpan2 703	. . . . . . . . . . . 12 ⊢ (𝑃:(0...2)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
8	7	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
9		1nn0 12515	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ₀
10		1le2 12447	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ≤ 2
11		elfz2nn0 13642	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ (0...2) ↔ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 1 ≤ 2))
12	9, 2, 10, 11	mpbir3an 1360	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ (0...2)
13		ffvelcdm 7076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...2)⟶𝑉 ∧ 1 ∈ (0...2)) → (𝑃‘1) ∈ 𝑉)
14	12, 13	mpan2 703	. . . . . . . . . . . . . . . 16 ⊢ (𝑃:(0...2)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
15	14	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
16		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → 𝐺 ∈ USGraph)
17		fvex 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃‘1) ∈ V
18	16, 17	jctir 529	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ USGraph ∧ (𝑃‘1) ∈ V))
19		prcom 4698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘0)}
20	19	eqeq2i 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘1), (𝑃‘0)})
21	20	birani 508	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐼‘(𝐹‘0)) = {(𝑃‘1), (𝑃‘0)})
22	21	ad2antlr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝐼‘(𝐹‘0)) = {(𝑃‘1), (𝑃‘0)})
23		usgr2pthlem.i	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐼 = (iEdg‘𝐺)
24	23	usgrnloopv 29550	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘1) ∈ V) → ((𝐼‘(𝐹‘0)) = {(𝑃‘1), (𝑃‘0)} → (𝑃‘1) ≠ (𝑃‘0)))
25	18, 22, 24	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝑃‘1) ≠ (𝑃‘0))
26	25	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘1) ≠ (𝑃‘0))
27	17	elsn 4604	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘1) ∈ {(𝑃‘0)} ↔ (𝑃‘1) = (𝑃‘0))
28	27	necon3bbii 3005	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑃‘1) ∈ {(𝑃‘0)} ↔ (𝑃‘1) ≠ (𝑃‘0))
29	26, 28	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ¬ (𝑃‘1) ∈ {(𝑃‘0)})
30	15, 29	eldifd 3916	. . . . . . . . . . . . . 14 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘1) ∈ (𝑉 ∖ {(𝑃‘0)}))
31	30	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) → (𝑃‘1) ∈ (𝑉 ∖ {(𝑃‘0)}))
32		sneq 4599	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑃‘0) → {𝑥} = {(𝑃‘0)})
33	32	difeq2d 4081	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑃‘0) → (𝑉 ∖ {𝑥}) = (𝑉 ∖ {(𝑃‘0)}))
34	33	eleq2d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑃‘0) → ((𝑃‘1) ∈ (𝑉 ∖ {𝑥}) ↔ (𝑃‘1) ∈ (𝑉 ∖ {(𝑃‘0)})))
35	34	adantl 486	. . . . . . . . . . . . 13 ⊢ (((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) → ((𝑃‘1) ∈ (𝑉 ∖ {𝑥}) ↔ (𝑃‘1) ∈ (𝑉 ∖ {(𝑃‘0)})))
36	31, 35	mpbird 260	. . . . . . . . . . . 12 ⊢ (((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) → (𝑃‘1) ∈ (𝑉 ∖ {𝑥}))
37		2re 12310	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
38	37	leidi 11743	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ 2
39		elfz2nn0 13642	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ (0...2) ↔ (2 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ∧ 2 ≤ 2))
40	2, 2, 38, 39	mpbir3an 1360	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ (0...2)
41		ffvelcdm 7076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃:(0...2)⟶𝑉 ∧ 2 ∈ (0...2)) → (𝑃‘2) ∈ 𝑉)
42	40, 41	mpan2 703	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃:(0...2)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
43	42	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
44	23	usgrf1 29522	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼–1-1→ran 𝐼)
45	44	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → 𝐼:dom 𝐼–1-1→ran 𝐼)
46		simpl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → 𝐹:(0..^2)–1-1→dom 𝐼)
47	46	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → 𝐹:(0..^2)–1-1→dom 𝐼)
48	45, 47	jca 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝐼:dom 𝐼–1-1→ran 𝐼 ∧ 𝐹:(0..^2)–1-1→dom 𝐼))
49		2nn 12309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℕ
50		lbfzo0 13724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ∈ (0..^2) ↔ 2 ∈ ℕ)
51	49, 50	mpbir 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ (0..^2)
52		1lt2 12408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
53		elfzo0 13725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ ∧ 1 < 2))
54	9, 49, 52, 53	mpbir3an 1360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ (0..^2)
55	51, 54	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ (0..^2) ∧ 1 ∈ (0..^2))
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (0 ∈ (0..^2) ∧ 1 ∈ (0..^2)))
57		0ne1 12307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≠ 1
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → 0 ≠ 1)
59	48, 56, 58	3jca 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝐼:dom 𝐼–1-1→ran 𝐼 ∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ (0 ∈ (0..^2) ∧ 1 ∈ (0..^2)) ∧ 0 ≠ 1))
60		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
61	60	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
62		2f1fvneq 7258	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐼:dom 𝐼–1-1→ran 𝐼 ∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ (0 ∈ (0..^2) ∧ 1 ∈ (0..^2)) ∧ 0 ≠ 1) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)}))
63	59, 61, 62	sylc 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)})
64		necom 3011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘0) ≠ (𝑃‘2))
65		fvex 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘0) ∈ V
66		fvex 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃‘2) ∈ V
67	65, 17, 66	3pm3.2i 1358	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃‘0) ∈ V ∧ (𝑃‘1) ∈ V ∧ (𝑃‘2) ∈ V)
68		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝑃‘0) ∈ V)
69		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})
70	69	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})
71	16, 68, 70	jca31 523	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) ∧ (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}))
72	71	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) ∧ (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}))
73	23	usgrnloopv 29550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1)))
74	73	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ USGraph ∧ (𝑃‘0) ∈ V) ∧ (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → (𝑃‘0) ≠ (𝑃‘1))
75	72, 74	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘0) ≠ (𝑃‘1))
76		pr1nebg 4823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑃‘0) ∈ V ∧ (𝑃‘1) ∈ V ∧ (𝑃‘2) ∈ V) ∧ (𝑃‘0) ≠ (𝑃‘1)) → ((𝑃‘0) ≠ (𝑃‘2) ↔ {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)}))
77	67, 75, 76	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝑃‘0) ≠ (𝑃‘2) ↔ {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)}))
78	64, 77	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝑃‘2) ≠ (𝑃‘0) ↔ {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)}))
79	63, 78	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘2) ≠ (𝑃‘0))
80		fvexd 6896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝑃‘2) ∈ V)
81		prcom 4698	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)}
82	81	eqeq2i 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)})
83	82	bilani 509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)})
84	83	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)})
85	16, 80, 84	jca31 523	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) → ((𝐺 ∈ USGraph ∧ (𝑃‘2) ∈ V) ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)}))
86	85	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ((𝐺 ∈ USGraph ∧ (𝑃‘2) ∈ V) ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)}))
87	23	usgrnloopv 29550	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ USGraph ∧ (𝑃‘2) ∈ V) → ((𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)} → (𝑃‘2) ≠ (𝑃‘1)))
88	87	imp 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ USGraph ∧ (𝑃‘2) ∈ V) ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)}) → (𝑃‘2) ≠ (𝑃‘1))
89	86, 88	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘2) ≠ (𝑃‘1))
90	79, 89	nelprd 4623	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → ¬ (𝑃‘2) ∈ {(𝑃‘0), (𝑃‘1)})
91	43, 90	eldifd 3916	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘2) ∈ (𝑉 ∖ {(𝑃‘0), (𝑃‘1)}))
92	91	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ ((((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) ∧ 𝑦 = (𝑃‘1)) → (𝑃‘2) ∈ (𝑉 ∖ {(𝑃‘0), (𝑃‘1)}))
93		preq12 4701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) → {𝑥, 𝑦} = {(𝑃‘0), (𝑃‘1)})
94	93	difeq2d 4081	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) → (𝑉 ∖ {𝑥, 𝑦}) = (𝑉 ∖ {(𝑃‘0), (𝑃‘1)}))
95	94	eleq2d 2849	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) → ((𝑃‘2) ∈ (𝑉 ∖ {𝑥, 𝑦}) ↔ (𝑃‘2) ∈ (𝑉 ∖ {(𝑃‘0), (𝑃‘1)})))
96	95	adantll 726	. . . . . . . . . . . . . 14 ⊢ ((((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) ∧ 𝑦 = (𝑃‘1)) → ((𝑃‘2) ∈ (𝑉 ∖ {𝑥, 𝑦}) ↔ (𝑃‘2) ∈ (𝑉 ∖ {(𝑃‘0), (𝑃‘1)})))
97	92, 96	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) ∧ 𝑦 = (𝑃‘1)) → (𝑃‘2) ∈ (𝑉 ∖ {𝑥, 𝑦}))
98		eqcom 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑃‘0) ↔ (𝑃‘0) = 𝑥)
99		eqcom 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑃‘1) ↔ (𝑃‘1) = 𝑦)
100		eqcom 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑃‘2) ↔ (𝑃‘2) = 𝑧)
101	98, 99, 100	3anbi123i 1173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1) ∧ 𝑧 = (𝑃‘2)) ↔ ((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧))
102	101	biimpi 219	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1) ∧ 𝑧 = (𝑃‘2)) → ((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧))
103	102	ad4ant123 1191	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → ((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧))
104	98	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑃‘0) → (𝑃‘0) = 𝑥)
105	104	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → (𝑃‘0) = 𝑥)
106	99	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑃‘1) → (𝑃‘1) = 𝑦)
107	106	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → (𝑃‘1) = 𝑦)
108	105, 107	preq12d 4707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → {(𝑃‘0), (𝑃‘1)} = {𝑥, 𝑦})
109	108	eqeq2d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ (𝐼‘(𝐹‘0)) = {𝑥, 𝑦}))
110	100	bilani 509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → (𝑃‘2) = 𝑧)
111	107, 110	preq12d 4707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → {(𝑃‘1), (𝑃‘2)} = {𝑦, 𝑧})
112	111	eqeq2d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → ((𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))
113	109, 112	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))
114	113	biimpa 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))
115	103, 114	jca 520	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 = (𝑃‘0) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))
116	115	exp41 439	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑃‘0) → (𝑦 = (𝑃‘1) → (𝑧 = (𝑃‘2) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
117	116	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) → (𝑦 = (𝑃‘1) → (𝑧 = (𝑃‘2) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
118	117	imp31 422	. . . . . . . . . . . . 13 ⊢ (((((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) ∧ 𝑦 = (𝑃‘1)) ∧ 𝑧 = (𝑃‘2)) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
119	97, 118	rspcimedv 3572	. . . . . . . . . . . 12 ⊢ ((((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) ∧ 𝑦 = (𝑃‘1)) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
120	36, 119	rspcimedv 3572	. . . . . . . . . . 11 ⊢ (((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) ∧ 𝑥 = (𝑃‘0)) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
121	8, 120	rspcimedv 3572	. . . . . . . . . 10 ⊢ ((((𝐹:(0..^2)–1-1→dom 𝐼 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) ∧ 𝐺 ∈ USGraph) ∧ 𝑃:(0...2)⟶𝑉) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
122	121	exp41 439	. . . . . . . . 9 ⊢ (𝐹:(0..^2)–1-1→dom 𝐼 → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐺 ∈ USGraph → (𝑃:(0...2)⟶𝑉 → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))))
123	122	com15 102	. . . . . . . 8 ⊢ (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐺 ∈ USGraph → (𝑃:(0...2)⟶𝑉 → (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))))
124	123	pm2.43i 53	. . . . . . 7 ⊢ (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐺 ∈ USGraph → (𝑃:(0...2)⟶𝑉 → (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
125	124	com12 33	. . . . . 6 ⊢ (𝐺 ∈ USGraph → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃:(0...2)⟶𝑉 → (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
126	125	adantr 485	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃:(0...2)⟶𝑉 → (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
127		oveq2 7418	. . . . . . . 8 ⊢ ((♯‘𝐹) = 2 → (0..^(♯‘𝐹)) = (0..^2))
128	127	raleqdv 3323	. . . . . . 7 ⊢ ((♯‘𝐹) = 2 → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^2)(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
129		fzo0to2pr 13775	. . . . . . . . 9 ⊢ (0..^2) = {0, 1}
130	129	raleqi 3321	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^2)(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})
131		2wlklem 30015	. . . . . . . 8 ⊢ (∀𝑖 ∈ {0, 1} (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
132	130, 131	bitri 278	. . . . . . 7 ⊢ (∀𝑖 ∈ (0..^2)(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
133	128, 132	bitrdi 290	. . . . . 6 ⊢ ((♯‘𝐹) = 2 → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))
134	133	adantl 486	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))
135		oveq2 7418	. . . . . . . 8 ⊢ ((♯‘𝐹) = 2 → (0...(♯‘𝐹)) = (0...2))
136	135	feq2d 6689	. . . . . . 7 ⊢ ((♯‘𝐹) = 2 → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉))
137	136	adantl 486	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝑃:(0...(♯‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉))
138		f1eq2 6770	. . . . . . . . 9 ⊢ ((0..^(♯‘𝐹)) = (0..^2) → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ↔ 𝐹:(0..^2)–1-1→dom 𝐼))
139	127, 138	syl 18	. . . . . . . 8 ⊢ ((♯‘𝐹) = 2 → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ↔ 𝐹:(0..^2)–1-1→dom 𝐼))
140	139	imbi1d 344	. . . . . . 7 ⊢ ((♯‘𝐹) = 2 → ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))
141	140	adantl 486	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))
142	137, 141	imbi12d 347	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ((𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) ↔ (𝑃:(0...2)⟶𝑉 → (𝐹:(0..^2)–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
143	126, 134, 142	3imtr4d 297	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
144	143	com14 97	. . 3 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
145	144	com23 87	. 2 ⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → (∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))))
146	145	3imp 1128	1 ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 Vcvv 3455 ∖ cdif 3902 {csn 4589 {cpr 4591 class class class wbr 5109 dom cdm 5661 ran crn 5662 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7410 0cc0 11095 1c1 11096 + caddc 11098 < clt 11238 ≤ cle 11239 ℕcn 12228 2c2 12290 ℕ₀cn0 12499 ...cfz 13530 ..^cfzo 13678 ♯chash 14362 Vtxcvtx 29346 iEdgciedg 29347 USGraphcusgr 29499

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-n0 12500 df-z 12587 df-uz 12858 df-fz 13531 df-fzo 13679 df-hash 14363 df-umgr 29433 df-usgr 29501

This theorem is referenced by: usgr2pth 30113

W3C validator