eupap1 - Metamath Proof Explorer

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

Theorem eupap1 26503

Description: Append one path segment to an Eulerian path (enlarging the graph to add the new edge). (Contributed by Mario Carneiro, 7-Apr-2015.)

**Hypotheses**
Ref	Expression
eupap1.e	⊢ (𝜑 → 𝐸 Fn 𝐴)
eupap1.a	⊢ (𝜑 → 𝐴 ∈ Fin)
eupap1.b	⊢ (𝜑 → 𝐵 ∈ V)
eupap1.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
eupap1.d	⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)
eupap1.g	⊢ (𝜑 → 𝐺(𝑉 EulPaths 𝐸)𝑃)
eupap1.n	⊢ (𝜑 → 𝑁 = (#‘𝐺))
eupap1.f	⊢ 𝐹 = (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
eupap1.h	⊢ 𝐻 = (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})
eupap1.q	⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})

**Assertion**
Ref	Expression
eupap1	⊢ (𝜑 → 𝐻(𝑉 EulPaths 𝐹)𝑄)

Proof of Theorem eupap1 Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eupap1.e	. . . 4 ⊢ (𝜑 → 𝐸 Fn 𝐴)
2		eupap1.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ V)
3		prex 4836	. . . . . 6 ⊢ {(𝑃‘𝑁), 𝐶} ∈ V
4		f1osng 6089	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ {(𝑃‘𝑁), 𝐶} ∈ V) → {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}:{𝐵}–1-1-onto→{{(𝑃‘𝑁), 𝐶}})
5	2, 3, 4	sylancl 693	. . . . 5 ⊢ (𝜑 → {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}:{𝐵}–1-1-onto→{{(𝑃‘𝑁), 𝐶}})
6		f1ofn 6051	. . . . 5 ⊢ ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}:{𝐵}–1-1-onto→{{(𝑃‘𝑁), 𝐶}} → {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} Fn {𝐵})
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} Fn {𝐵})
8		eupap1.d	. . . . 5 ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)
9		disjsn 4192	. . . . 5 ⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴)
10	8, 9	sylibr 223	. . . 4 ⊢ (𝜑 → (𝐴 ∩ {𝐵}) = ∅)
11		eupap1.g	. . . . 5 ⊢ (𝜑 → 𝐺(𝑉 EulPaths 𝐸)𝑃)
12		eupagra 26493	. . . . 5 ⊢ (𝐺(𝑉 EulPaths 𝐸)𝑃 → 𝑉 UMGrph 𝐸)
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → 𝑉 UMGrph 𝐸)
14		relumgra 25843	. . . . . . 7 ⊢ Rel UMGrph
15	14	brrelexi 5082	. . . . . 6 ⊢ (𝑉 UMGrph 𝐸 → 𝑉 ∈ V)
16	13, 15	syl 17	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ V)
17		eupapf 26499	. . . . . . 7 ⊢ (𝐺(𝑉 EulPaths 𝐸)𝑃 → 𝑃:(0...(#‘𝐺))⟶𝑉)
18	11, 17	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃:(0...(#‘𝐺))⟶𝑉)
19		eupap1.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (#‘𝐺))
20		eupacl 26496	. . . . . . . . . . 11 ⊢ (𝐺(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐺) ∈ ℕ₀)
21	11, 20	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐺) ∈ ℕ₀)
22	19, 21	eqeltrd 2688	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
23		nn0uz 11598	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
24	22, 23	syl6eleq 2698	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
25		eluzfz2 12220	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
26	24, 25	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
27	19	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) = (0...(#‘𝐺)))
28	26, 27	eleqtrd 2690	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐺)))
29	18, 28	ffvelrnd 6268	. . . . 5 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
30		eupap1.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
31		umgra1 25855	. . . . 5 ⊢ (((𝑉 ∈ V ∧ 𝐵 ∈ V) ∧ ((𝑃‘𝑁) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 UMGrph {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
32	16, 2, 29, 30, 31	syl22anc 1319	. . . 4 ⊢ (𝜑 → 𝑉 UMGrph {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
33	1, 7, 10, 13, 32	umgraun 25857	. . 3 ⊢ (𝜑 → 𝑉 UMGrph (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}))
34		eupap1.f	. . 3 ⊢ 𝐹 = (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
35	33, 34	syl6breqr 4625	. 2 ⊢ (𝜑 → 𝑉 UMGrph 𝐹)
36		peano2nn0 11210	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
37	22, 36	syl 17	. . 3 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
38		eupaf1o 26497	. . . . . . . 8 ⊢ ((𝐺(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐺:(1...(#‘𝐺))–1-1-onto→𝐴)
39	11, 1, 38	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → 𝐺:(1...(#‘𝐺))–1-1-onto→𝐴)
40	19	oveq2d 6565	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) = (1...(#‘𝐺)))
41		f1oeq2 6041	. . . . . . . 8 ⊢ ((1...𝑁) = (1...(#‘𝐺)) → (𝐺:(1...𝑁)–1-1-onto→𝐴 ↔ 𝐺:(1...(#‘𝐺))–1-1-onto→𝐴))
42	40, 41	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐺:(1...𝑁)–1-1-onto→𝐴 ↔ 𝐺:(1...(#‘𝐺))–1-1-onto→𝐴))
43	39, 42	mpbird 246	. . . . . 6 ⊢ (𝜑 → 𝐺:(1...𝑁)–1-1-onto→𝐴)
44		f1osng 6089	. . . . . . 7 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐵 ∈ V) → {⟨(𝑁 + 1), 𝐵⟩}:{(𝑁 + 1)}–1-1-onto→{𝐵})
45	37, 2, 44	syl2anc 691	. . . . . 6 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐵⟩}:{(𝑁 + 1)}–1-1-onto→{𝐵})
46		fzp1disj 12269	. . . . . . 7 ⊢ ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅
47	46	a1i 11	. . . . . 6 ⊢ (𝜑 → ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅)
48		f1oun 6069	. . . . . 6 ⊢ (((𝐺:(1...𝑁)–1-1-onto→𝐴 ∧ {⟨(𝑁 + 1), 𝐵⟩}:{(𝑁 + 1)}–1-1-onto→{𝐵}) ∧ (((1...𝑁) ∩ {(𝑁 + 1)}) = ∅ ∧ (𝐴 ∩ {𝐵}) = ∅)) → (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
49	43, 45, 47, 10, 48	syl22anc 1319	. . . . 5 ⊢ (𝜑 → (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
50		eupap1.h	. . . . . 6 ⊢ 𝐻 = (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})
51		f1oeq1 6040	. . . . . 6 ⊢ (𝐻 = (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}) → (𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}) ↔ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵})))
52	50, 51	ax-mp 5	. . . . 5 ⊢ (𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}) ↔ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
53	49, 52	sylibr 223	. . . 4 ⊢ (𝜑 → 𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
54		1z 11284	. . . . . 6 ⊢ 1 ∈ ℤ
55		1m1e0 10966	. . . . . . . 8 ⊢ (1 − 1) = 0
56	55	fveq2i 6106	. . . . . . 7 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
57	24, 56	syl6eleqr 2699	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
58		fzsuc2 12268	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
59	54, 57, 58	sylancr 694	. . . . 5 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
60		f1oeq2 6041	. . . . 5 ⊢ ((1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}) → (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵})))
61	59, 60	syl 17	. . . 4 ⊢ (𝜑 → (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵})))
62	53, 61	mpbird 246	. . 3 ⊢ (𝜑 → 𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}))
63	27	feq2d 5944	. . . . . 6 ⊢ (𝜑 → (𝑃:(0...𝑁)⟶𝑉 ↔ 𝑃:(0...(#‘𝐺))⟶𝑉))
64	18, 63	mpbird 246	. . . . 5 ⊢ (𝜑 → 𝑃:(0...𝑁)⟶𝑉)
65		f1osng 6089	. . . . . . . 8 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐶 ∈ 𝑉) → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶})
66	37, 30, 65	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶})
67		f1of 6050	. . . . . . 7 ⊢ ({⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶} → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶{𝐶})
68	66, 67	syl 17	. . . . . 6 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶{𝐶})
69	30	snssd 4281	. . . . . 6 ⊢ (𝜑 → {𝐶} ⊆ 𝑉)
70	68, 69	fssd 5970	. . . . 5 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶𝑉)
71		fzp1disj 12269	. . . . . 6 ⊢ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅
72	71	a1i 11	. . . . 5 ⊢ (𝜑 → ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅)
73		fun2 5980	. . . . 5 ⊢ (((𝑃:(0...𝑁)⟶𝑉 ∧ {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶𝑉) ∧ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉)
74	64, 70, 72, 73	syl21anc 1317	. . . 4 ⊢ (𝜑 → (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉)
75		eupap1.q	. . . . . 6 ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
76	75	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
77		fzsuc 12258	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)}))
78	24, 77	syl 17	. . . . 5 ⊢ (𝜑 → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)}))
79	76, 78	feq12d 5946	. . . 4 ⊢ (𝜑 → (𝑄:(0...(𝑁 + 1))⟶𝑉 ↔ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉))
80	74, 79	mpbird 246	. . 3 ⊢ (𝜑 → 𝑄:(0...(𝑁 + 1))⟶𝑉)
81	34	fveq1i 6104	. . . . . . . 8 ⊢ (𝐹‘(𝐺‘𝑘)) = ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘(𝐺‘𝑘))
82		f1of 6050	. . . . . . . . . . . . 13 ⊢ (𝐺:(1...𝑁)–1-1-onto→𝐴 → 𝐺:(1...𝑁)⟶𝐴)
83	43, 82	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...𝑁)⟶𝐴)
84	83	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐺‘𝑘) ∈ 𝐴)
85	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝐵 ∈ 𝐴)
86		nelne2 2879	. . . . . . . . . . 11 ⊢ (((𝐺‘𝑘) ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐺‘𝑘) ≠ 𝐵)
87	84, 85, 86	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐺‘𝑘) ≠ 𝐵)
88	87	necomd 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝐵 ≠ (𝐺‘𝑘))
89		fvunsn 6350	. . . . . . . . 9 ⊢ (𝐵 ≠ (𝐺‘𝑘) → ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘)))
90	88, 89	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘)))
91	81, 90	syl5eq 2656	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘)))
92	50	fveq1i 6104	. . . . . . . . 9 ⊢ (𝐻‘𝑘) = ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘)
93		elfznn 12241	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
94	93	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
95	94	nnred 10912	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℝ)
96	22	nn0red 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
97	96	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
98	37	nn0red 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ∈ ℝ)
100		elfzle2 12216	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ≤ 𝑁)
101	100	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ≤ 𝑁)
102	96	ltp1d 10833	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
103	102	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑁 < (𝑁 + 1))
104	95, 97, 99, 101, 103	lelttrd 10074	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 < (𝑁 + 1))
105	95, 104	gtned 10051	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ≠ 𝑘)
106		fvunsn 6350	. . . . . . . . . 10 ⊢ ((𝑁 + 1) ≠ 𝑘 → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘) = (𝐺‘𝑘))
107	105, 106	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘) = (𝐺‘𝑘))
108	92, 107	syl5eq 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐻‘𝑘) = (𝐺‘𝑘))
109	108	fveq2d 6107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
110	75	fveq1i 6104	. . . . . . . . . 10 ⊢ (𝑄‘(𝑘 − 1)) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1))
111		peano2rem 10227	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℝ → (𝑘 − 1) ∈ ℝ)
112	95, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℝ)
113	95	ltm1d 10835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) < 𝑘)
114	112, 95, 99, 113, 104	lttrd 10077	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) < (𝑁 + 1))
115	112, 114	gtned 10051	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ≠ (𝑘 − 1))
116		fvunsn 6350	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ≠ (𝑘 − 1) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
118	110, 117	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑄‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
119	75	fveq1i 6104	. . . . . . . . . 10 ⊢ (𝑄‘𝑘) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘)
120		fvunsn 6350	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ≠ 𝑘 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘) = (𝑃‘𝑘))
121	105, 120	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘) = (𝑃‘𝑘))
122	119, 121	syl5eq 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑄‘𝑘) = (𝑃‘𝑘))
123	118, 122	preq12d 4220	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})
124	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝐺(𝑉 EulPaths 𝐸)𝑃)
125	40	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ (1...𝑁) ↔ 𝑘 ∈ (1...(#‘𝐺))))
126	125	biimpa 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ (1...(#‘𝐺)))
127		eupaseg 26500	. . . . . . . . 9 ⊢ ((𝐺(𝑉 EulPaths 𝐸)𝑃 ∧ 𝑘 ∈ (1...(#‘𝐺))) → (𝐸‘(𝐺‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})
128	124, 126, 127	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐸‘(𝐺‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})
129	123, 128	eqtr4d 2647	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} = (𝐸‘(𝐺‘𝑘)))
130	91, 109, 129	3eqtr4d 2654	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
131	130	ralrimiva 2949	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
132	34	fveq1i 6104	. . . . . . . . . 10 ⊢ (𝐹‘𝐵) = ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘𝐵)
133		fnun 5911	. . . . . . . . . . . . 13 ⊢ (((𝐸 Fn 𝐴 ∧ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} Fn {𝐵}) ∧ (𝐴 ∩ {𝐵}) = ∅) → (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
134	1, 7, 10, 133	syl21anc 1317	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
135		fnfun 5902	. . . . . . . . . . . 12 ⊢ ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}) → Fun (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}))
136	134, 135	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}))
137		ssun2 3739	. . . . . . . . . . . 12 ⊢ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
138	137	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}))
139		snidg 4153	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐵})
140	2, 139	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
141	3	dmsnop 5527	. . . . . . . . . . . 12 ⊢ dom {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} = {𝐵}
142	140, 141	syl6eleqr 2699	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ dom {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})
143		funssfv 6119	. . . . . . . . . . 11 ⊢ ((Fun (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) ∧ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) ∧ 𝐵 ∈ dom {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) → ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘𝐵) = ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}‘𝐵))
144	136, 138, 142, 143	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩})‘𝐵) = ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}‘𝐵))
145	132, 144	syl5eq 2656	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝐵) = ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}‘𝐵))
146		fvsng 6352	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ {(𝑃‘𝑁), 𝐶} ∈ V) → ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}‘𝐵) = {(𝑃‘𝑁), 𝐶})
147	2, 3, 146	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → ({⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}‘𝐵) = {(𝑃‘𝑁), 𝐶})
148	145, 147	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐵) = {(𝑃‘𝑁), 𝐶})
149	50	fveq1i 6104	. . . . . . . . . . 11 ⊢ (𝐻‘(𝑁 + 1)) = ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1))
150		f1ofun 6052	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}) → Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
151	49, 150	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
152		ssun2 3739	. . . . . . . . . . . . 13 ⊢ {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})
153	152	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
154		snidg 4153	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝑁 + 1) ∈ {(𝑁 + 1)})
155	37, 154	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ {(𝑁 + 1)})
156		dmsnopg 5524	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ V → dom {⟨(𝑁 + 1), 𝐵⟩} = {(𝑁 + 1)})
157	2, 156	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom {⟨(𝑁 + 1), 𝐵⟩} = {(𝑁 + 1)})
158	155, 157	eleqtrrd 2691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐵⟩})
159		funssfv 6119	. . . . . . . . . . . 12 ⊢ ((Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}) ∧ {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}) ∧ (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐵⟩}) → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
160	151, 153, 158, 159	syl3anc 1318	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
161	149, 160	syl5eq 2656	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
162		fvsng 6352	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐵 ∈ V) → ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)) = 𝐵)
163	37, 2, 162	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)) = 𝐵)
164	161, 163	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘(𝑁 + 1)) = 𝐵)
165	164	fveq2d 6107	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝐻‘(𝑁 + 1))) = (𝐹‘𝐵))
166	96	recnd 9947	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
167		ax-1cn 9873	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
168		pncan 10166	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
169	166, 167, 168	sylancl 693	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
170	169	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘((𝑁 + 1) − 1)) = (𝑄‘𝑁))
171	75	fveq1i 6104	. . . . . . . . . . 11 ⊢ (𝑄‘𝑁) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁)
172	96, 102	gtned 10051	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ≠ 𝑁)
173		fvunsn 6350	. . . . . . . . . . . 12 ⊢ ((𝑁 + 1) ≠ 𝑁 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁) = (𝑃‘𝑁))
174	172, 173	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁) = (𝑃‘𝑁))
175	171, 174	syl5eq 2656	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑁) = (𝑃‘𝑁))
176	170, 175	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘((𝑁 + 1) − 1)) = (𝑃‘𝑁))
177	75	fveq1i 6104	. . . . . . . . . . 11 ⊢ (𝑄‘(𝑁 + 1)) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1))
178		ffun 5961	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉 → Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
179	74, 178	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
180		ssun2 3739	. . . . . . . . . . . . 13 ⊢ {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
181	180	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
182		dmsnopg 5524	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝑉 → dom {⟨(𝑁 + 1), 𝐶⟩} = {(𝑁 + 1)})
183	30, 182	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom {⟨(𝑁 + 1), 𝐶⟩} = {(𝑁 + 1)})
184	155, 183	eleqtrrd 2691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐶⟩})
185		funssfv 6119	. . . . . . . . . . . 12 ⊢ ((Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}) ∧ {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}) ∧ (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐶⟩}) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
186	179, 181, 184, 185	syl3anc 1318	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
187	177, 186	syl5eq 2656	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
188		fvsng 6352	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐶 ∈ 𝑉) → ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)) = 𝐶)
189	37, 30, 188	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)) = 𝐶)
190	187, 189	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘(𝑁 + 1)) = 𝐶)
191	176, 190	preq12d 4220	. . . . . . . 8 ⊢ (𝜑 → {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))} = {(𝑃‘𝑁), 𝐶})
192	148, 165, 191	3eqtr4d 2654	. . . . . . 7 ⊢ (𝜑 → (𝐹‘(𝐻‘(𝑁 + 1))) = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))})
193		elsni 4142	. . . . . . . . . 10 ⊢ (𝑘 ∈ {(𝑁 + 1)} → 𝑘 = (𝑁 + 1))
194	193	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑘 ∈ {(𝑁 + 1)} → (𝐻‘𝑘) = (𝐻‘(𝑁 + 1)))
195	194	fveq2d 6107	. . . . . . . 8 ⊢ (𝑘 ∈ {(𝑁 + 1)} → (𝐹‘(𝐻‘𝑘)) = (𝐹‘(𝐻‘(𝑁 + 1))))
196	193	oveq1d 6564	. . . . . . . . . 10 ⊢ (𝑘 ∈ {(𝑁 + 1)} → (𝑘 − 1) = ((𝑁 + 1) − 1))
197	196	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑘 ∈ {(𝑁 + 1)} → (𝑄‘(𝑘 − 1)) = (𝑄‘((𝑁 + 1) − 1)))
198	193	fveq2d 6107	. . . . . . . . 9 ⊢ (𝑘 ∈ {(𝑁 + 1)} → (𝑄‘𝑘) = (𝑄‘(𝑁 + 1)))
199	197, 198	preq12d 4220	. . . . . . . 8 ⊢ (𝑘 ∈ {(𝑁 + 1)} → {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))})
200	195, 199	eqeq12d 2625	. . . . . . 7 ⊢ (𝑘 ∈ {(𝑁 + 1)} → ((𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} ↔ (𝐹‘(𝐻‘(𝑁 + 1))) = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))}))
201	192, 200	syl5ibrcom 236	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ {(𝑁 + 1)} → (𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))
202	201	ralrimiv 2948	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {(𝑁 + 1)} (𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
203		ralun 3757	. . . . 5 ⊢ ((∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} ∧ ∀𝑘 ∈ {(𝑁 + 1)} (𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}) → ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
204	131, 202, 203	syl2anc 691	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
205	59	raleqdv 3121	. . . 4 ⊢ (𝜑 → (∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} ↔ ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))
206	204, 205	mpbird 246	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})
207		oveq2 6557	. . . . . 6 ⊢ (𝑛 = (𝑁 + 1) → (1...𝑛) = (1...(𝑁 + 1)))
208		f1oeq2 6041	. . . . . 6 ⊢ ((1...𝑛) = (1...(𝑁 + 1)) → (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵})))
209	207, 208	syl 17	. . . . 5 ⊢ (𝑛 = (𝑁 + 1) → (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵})))
210		oveq2 6557	. . . . . 6 ⊢ (𝑛 = (𝑁 + 1) → (0...𝑛) = (0...(𝑁 + 1)))
211	210	feq2d 5944	. . . . 5 ⊢ (𝑛 = (𝑁 + 1) → (𝑄:(0...𝑛)⟶𝑉 ↔ 𝑄:(0...(𝑁 + 1))⟶𝑉))
212	207	raleqdv 3121	. . . . 5 ⊢ (𝑛 = (𝑁 + 1) → (∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} ↔ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))
213	209, 211, 212	3anbi123d 1391	. . . 4 ⊢ (𝑛 = (𝑁 + 1) → ((𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}) ↔ (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...(𝑁 + 1))⟶𝑉 ∧ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})))
214	213	rspcev 3282	. . 3 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...(𝑁 + 1))⟶𝑉 ∧ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})) → ∃𝑛 ∈ ℕ₀ (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))
215	37, 62, 80, 206, 214	syl13anc 1320	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))
216	34	fneq1i 5899	. . . . 5 ⊢ (𝐹 Fn (𝐴 ∪ {𝐵}) ↔ (𝐸 ∪ {⟨𝐵, {(𝑃‘𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
217	134, 216	sylibr 223	. . . 4 ⊢ (𝜑 → 𝐹 Fn (𝐴 ∪ {𝐵}))
218		fndm 5904	. . . 4 ⊢ (𝐹 Fn (𝐴 ∪ {𝐵}) → dom 𝐹 = (𝐴 ∪ {𝐵}))
219	217, 218	syl 17	. . 3 ⊢ (𝜑 → dom 𝐹 = (𝐴 ∪ {𝐵}))
220		iseupa 26492	. . 3 ⊢ (dom 𝐹 = (𝐴 ∪ {𝐵}) → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ₀ (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))))
221	219, 220	syl 17	. 2 ⊢ (𝜑 → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ₀ (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))))
222	35, 215, 221	mpbir2and 959	1 ⊢ (𝜑 → 𝐻(𝑉 EulPaths 𝐹)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 {csn 4125 {cpr 4127 ⟨cop 4131 class class class wbr 4583 dom cdm 5038 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 #chash 12979 UMGrph cumg 25841 EulPaths ceup 26489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-fz 12198 df-hash 12980 df-umgra 25842 df-eupa 26490

This theorem is referenced by: (None)

W3C validator