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.
StepHypRef 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→{{(𝑃𝑁), 𝐶}})
52, 3, 4sylancl 693 . . . . 5 (𝜑 → {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}:{𝐵}–1-1-onto→{{(𝑃𝑁), 𝐶}})
6 f1ofn 6051 . . . . 5 ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}:{𝐵}–1-1-onto→{{(𝑃𝑁), 𝐶}} → {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} Fn {𝐵})
75, 6syl 17 . . . 4 (𝜑 → {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} Fn {𝐵})
8 eupap1.d . . . . 5 (𝜑 → ¬ 𝐵𝐴)
9 disjsn 4192 . . . . 5 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
108, 9sylibr 223 . . . 4 (𝜑 → (𝐴 ∩ {𝐵}) = ∅)
11 eupap1.g . . . . 5 (𝜑𝐺(𝑉 EulPaths 𝐸)𝑃)
12 eupagra 26493 . . . . 5 (𝐺(𝑉 EulPaths 𝐸)𝑃𝑉 UMGrph 𝐸)
1311, 12syl 17 . . . 4 (𝜑𝑉 UMGrph 𝐸)
14 relumgra 25843 . . . . . . 7 Rel UMGrph
1514brrelexi 5082 . . . . . 6 (𝑉 UMGrph 𝐸𝑉 ∈ V)
1613, 15syl 17 . . . . 5 (𝜑𝑉 ∈ V)
17 eupapf 26499 . . . . . . 7 (𝐺(𝑉 EulPaths 𝐸)𝑃𝑃:(0...(#‘𝐺))⟶𝑉)
1811, 17syl 17 . . . . . 6 (𝜑𝑃:(0...(#‘𝐺))⟶𝑉)
19 eupap1.n . . . . . . . . . 10 (𝜑𝑁 = (#‘𝐺))
20 eupacl 26496 . . . . . . . . . . 11 (𝐺(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐺) ∈ ℕ0)
2111, 20syl 17 . . . . . . . . . 10 (𝜑 → (#‘𝐺) ∈ ℕ0)
2219, 21eqeltrd 2688 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
23 nn0uz 11598 . . . . . . . . 9 0 = (ℤ‘0)
2422, 23syl6eleq 2698 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘0))
25 eluzfz2 12220 . . . . . . . 8 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
2624, 25syl 17 . . . . . . 7 (𝜑𝑁 ∈ (0...𝑁))
2719oveq2d 6565 . . . . . . 7 (𝜑 → (0...𝑁) = (0...(#‘𝐺)))
2826, 27eleqtrd 2690 . . . . . 6 (𝜑𝑁 ∈ (0...(#‘𝐺)))
2918, 28ffvelrnd 6268 . . . . 5 (𝜑 → (𝑃𝑁) ∈ 𝑉)
30 eupap1.c . . . . 5 (𝜑𝐶𝑉)
31 umgra1 25855 . . . . 5 (((𝑉 ∈ V ∧ 𝐵 ∈ V) ∧ ((𝑃𝑁) ∈ 𝑉𝐶𝑉)) → 𝑉 UMGrph {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})
3216, 2, 29, 30, 31syl22anc 1319 . . . 4 (𝜑𝑉 UMGrph {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})
331, 7, 10, 13, 32umgraun 25857 . . 3 (𝜑𝑉 UMGrph (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}))
34 eupap1.f . . 3 𝐹 = (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})
3533, 34syl6breqr 4625 . 2 (𝜑𝑉 UMGrph 𝐹)
36 peano2nn0 11210 . . . 4 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
3722, 36syl 17 . . 3 (𝜑 → (𝑁 + 1) ∈ ℕ0)
38 eupaf1o 26497 . . . . . . . 8 ((𝐺(𝑉 EulPaths 𝐸)𝑃𝐸 Fn 𝐴) → 𝐺:(1...(#‘𝐺))–1-1-onto𝐴)
3911, 1, 38syl2anc 691 . . . . . . 7 (𝜑𝐺:(1...(#‘𝐺))–1-1-onto𝐴)
4019oveq2d 6565 . . . . . . . 8 (𝜑 → (1...𝑁) = (1...(#‘𝐺)))
41 f1oeq2 6041 . . . . . . . 8 ((1...𝑁) = (1...(#‘𝐺)) → (𝐺:(1...𝑁)–1-1-onto𝐴𝐺:(1...(#‘𝐺))–1-1-onto𝐴))
4240, 41syl 17 . . . . . . 7 (𝜑 → (𝐺:(1...𝑁)–1-1-onto𝐴𝐺:(1...(#‘𝐺))–1-1-onto𝐴))
4339, 42mpbird 246 . . . . . 6 (𝜑𝐺:(1...𝑁)–1-1-onto𝐴)
44 f1osng 6089 . . . . . . 7 (((𝑁 + 1) ∈ ℕ0𝐵 ∈ V) → {⟨(𝑁 + 1), 𝐵⟩}:{(𝑁 + 1)}–1-1-onto→{𝐵})
4537, 2, 44syl2anc 691 . . . . . 6 (𝜑 → {⟨(𝑁 + 1), 𝐵⟩}:{(𝑁 + 1)}–1-1-onto→{𝐵})
46 fzp1disj 12269 . . . . . . 7 ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅
4746a1i 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→(𝐴 ∪ {𝐵}))
4943, 45, 47, 10, 48syl22anc 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→(𝐴 ∪ {𝐵})))
5250, 51ax-mp 5 . . . . 5 (𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}) ↔ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
5349, 52sylibr 223 . . . 4 (𝜑𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}))
54 1z 11284 . . . . . 6 1 ∈ ℤ
55 1m1e0 10966 . . . . . . . 8 (1 − 1) = 0
5655fveq2i 6106 . . . . . . 7 (ℤ‘(1 − 1)) = (ℤ‘0)
5724, 56syl6eleqr 2699 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘(1 − 1)))
58 fzsuc2 12268 . . . . . 6 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
5954, 57, 58sylancr 694 . . . . 5 (𝜑 → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
60 f1oeq2 6041 . . . . 5 ((1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}) → (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵})))
6159, 60syl 17 . . . 4 (𝜑 → (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵})))
6253, 61mpbird 246 . . 3 (𝜑𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}))
6327feq2d 5944 . . . . . 6 (𝜑 → (𝑃:(0...𝑁)⟶𝑉𝑃:(0...(#‘𝐺))⟶𝑉))
6418, 63mpbird 246 . . . . 5 (𝜑𝑃:(0...𝑁)⟶𝑉)
65 f1osng 6089 . . . . . . . 8 (((𝑁 + 1) ∈ ℕ0𝐶𝑉) → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶})
6637, 30, 65syl2anc 691 . . . . . . 7 (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶})
67 f1of 6050 . . . . . . 7 ({⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}–1-1-onto→{𝐶} → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶{𝐶})
6866, 67syl 17 . . . . . 6 (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶{𝐶})
6930snssd 4281 . . . . . 6 (𝜑 → {𝐶} ⊆ 𝑉)
7068, 69fssd 5970 . . . . 5 (𝜑 → {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶𝑉)
71 fzp1disj 12269 . . . . . 6 ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅
7271a1i 11 . . . . 5 (𝜑 → ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅)
73 fun2 5980 . . . . 5 (((𝑃:(0...𝑁)⟶𝑉 ∧ {⟨(𝑁 + 1), 𝐶⟩}:{(𝑁 + 1)}⟶𝑉) ∧ ((0...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉)
7464, 70, 72, 73syl21anc 1317 . . . 4 (𝜑 → (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉)
75 eupap1.q . . . . . 6 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
7675a1i 11 . . . . 5 (𝜑𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
77 fzsuc 12258 . . . . . 6 (𝑁 ∈ (ℤ‘0) → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)}))
7824, 77syl 17 . . . . 5 (𝜑 → (0...(𝑁 + 1)) = ((0...𝑁) ∪ {(𝑁 + 1)}))
7976, 78feq12d 5946 . . . 4 (𝜑 → (𝑄:(0...(𝑁 + 1))⟶𝑉 ↔ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉))
8074, 79mpbird 246 . . 3 (𝜑𝑄:(0...(𝑁 + 1))⟶𝑉)
8134fveq1i 6104 . . . . . . . 8 (𝐹‘(𝐺𝑘)) = ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘(𝐺𝑘))
82 f1of 6050 . . . . . . . . . . . . 13 (𝐺:(1...𝑁)–1-1-onto𝐴𝐺:(1...𝑁)⟶𝐴)
8343, 82syl 17 . . . . . . . . . . . 12 (𝜑𝐺:(1...𝑁)⟶𝐴)
8483ffvelrnda 6267 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐺𝑘) ∈ 𝐴)
858adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...𝑁)) → ¬ 𝐵𝐴)
86 nelne2 2879 . . . . . . . . . . 11 (((𝐺𝑘) ∈ 𝐴 ∧ ¬ 𝐵𝐴) → (𝐺𝑘) ≠ 𝐵)
8784, 85, 86syl2anc 691 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐺𝑘) ≠ 𝐵)
8887necomd 2837 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → 𝐵 ≠ (𝐺𝑘))
89 fvunsn 6350 . . . . . . . . 9 (𝐵 ≠ (𝐺𝑘) → ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘(𝐺𝑘)) = (𝐸‘(𝐺𝑘)))
9088, 89syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (1...𝑁)) → ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘(𝐺𝑘)) = (𝐸‘(𝐺𝑘)))
9181, 90syl5eq 2656 . . . . . . 7 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐺𝑘)) = (𝐸‘(𝐺𝑘)))
9250fveq1i 6104 . . . . . . . . 9 (𝐻𝑘) = ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘)
93 elfznn 12241 . . . . . . . . . . . . 13 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
9493adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
9594nnred 10912 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℝ)
9622nn0red 11229 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
9796adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
9837nn0red 11229 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℝ)
9998adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ∈ ℝ)
100 elfzle2 12216 . . . . . . . . . . . . 13 (𝑘 ∈ (1...𝑁) → 𝑘𝑁)
101100adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑘𝑁)
10296ltp1d 10833 . . . . . . . . . . . . 13 (𝜑𝑁 < (𝑁 + 1))
103102adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑁 < (𝑁 + 1))
10495, 97, 99, 101, 103lelttrd 10074 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑘 < (𝑁 + 1))
10595, 104gtned 10051 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ≠ 𝑘)
106 fvunsn 6350 . . . . . . . . . 10 ((𝑁 + 1) ≠ 𝑘 → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘) = (𝐺𝑘))
107105, 106syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘𝑘) = (𝐺𝑘))
10892, 107syl5eq 2656 . . . . . . . 8 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐻𝑘) = (𝐺𝑘))
109108fveq2d 6107 . . . . . . 7 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻𝑘)) = (𝐹‘(𝐺𝑘)))
11075fveq1i 6104 . . . . . . . . . 10 (𝑄‘(𝑘 − 1)) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1))
111 peano2rem 10227 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 − 1) ∈ ℝ)
11295, 111syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℝ)
11395ltm1d 10835 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑘 − 1) < 𝑘)
114112, 95, 99, 113, 104lttrd 10077 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑘 − 1) < (𝑁 + 1))
115112, 114gtned 10051 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑁 + 1) ≠ (𝑘 − 1))
116 fvunsn 6350 . . . . . . . . . . 11 ((𝑁 + 1) ≠ (𝑘 − 1) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
117115, 116syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...𝑁)) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
118110, 117syl5eq 2656 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑄‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
11975fveq1i 6104 . . . . . . . . . 10 (𝑄𝑘) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘)
120 fvunsn 6350 . . . . . . . . . . 11 ((𝑁 + 1) ≠ 𝑘 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘) = (𝑃𝑘))
121105, 120syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...𝑁)) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑘) = (𝑃𝑘))
122119, 121syl5eq 2656 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → (𝑄𝑘) = (𝑃𝑘))
123118, 122preq12d 4220 . . . . . . . 8 ((𝜑𝑘 ∈ (1...𝑁)) → {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})
12411adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → 𝐺(𝑉 EulPaths 𝐸)𝑃)
12540eleq2d 2673 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ (1...𝑁) ↔ 𝑘 ∈ (1...(#‘𝐺))))
126125biimpa 500 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → 𝑘 ∈ (1...(#‘𝐺)))
127 eupaseg 26500 . . . . . . . . 9 ((𝐺(𝑉 EulPaths 𝐸)𝑃𝑘 ∈ (1...(#‘𝐺))) → (𝐸‘(𝐺𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})
128124, 126, 127syl2anc 691 . . . . . . . 8 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐸‘(𝐺𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})
129123, 128eqtr4d 2647 . . . . . . 7 ((𝜑𝑘 ∈ (1...𝑁)) → {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} = (𝐸‘(𝐺𝑘)))
13091, 109, 1293eqtr4d 2654 . . . . . 6 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})
131130ralrimiva 2949 . . . . 5 (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})
13234fveq1i 6104 . . . . . . . . . 10 (𝐹𝐵) = ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘𝐵)
133 fnun 5911 . . . . . . . . . . . . 13 (((𝐸 Fn 𝐴 ∧ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} Fn {𝐵}) ∧ (𝐴 ∩ {𝐵}) = ∅) → (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
1341, 7, 10, 133syl21anc 1317 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
135 fnfun 5902 . . . . . . . . . . . 12 ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}) → Fun (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}))
136134, 135syl 17 . . . . . . . . . . 11 (𝜑 → Fun (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}))
137 ssun2 3739 . . . . . . . . . . . 12 {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})
138137a1i 11 . . . . . . . . . . 11 (𝜑 → {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}))
139 snidg 4153 . . . . . . . . . . . . 13 (𝐵 ∈ V → 𝐵 ∈ {𝐵})
1402, 139syl 17 . . . . . . . . . . . 12 (𝜑𝐵 ∈ {𝐵})
1413dmsnop 5527 . . . . . . . . . . . 12 dom {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} = {𝐵}
142140, 141syl6eleqr 2699 . . . . . . . . . . 11 (𝜑𝐵 ∈ dom {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})
143 funssfv 6119 . . . . . . . . . . 11 ((Fun (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) ∧ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩} ⊆ (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) ∧ 𝐵 ∈ dom {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) → ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘𝐵) = ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}‘𝐵))
144136, 138, 142, 143syl3anc 1318 . . . . . . . . . 10 (𝜑 → ((𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩})‘𝐵) = ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}‘𝐵))
145132, 144syl5eq 2656 . . . . . . . . 9 (𝜑 → (𝐹𝐵) = ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}‘𝐵))
146 fvsng 6352 . . . . . . . . . 10 ((𝐵 ∈ V ∧ {(𝑃𝑁), 𝐶} ∈ V) → ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}‘𝐵) = {(𝑃𝑁), 𝐶})
1472, 3, 146sylancl 693 . . . . . . . . 9 (𝜑 → ({⟨𝐵, {(𝑃𝑁), 𝐶}⟩}‘𝐵) = {(𝑃𝑁), 𝐶})
148145, 147eqtrd 2644 . . . . . . . 8 (𝜑 → (𝐹𝐵) = {(𝑃𝑁), 𝐶})
14950fveq1i 6104 . . . . . . . . . . 11 (𝐻‘(𝑁 + 1)) = ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1))
150 f1ofun 6052 . . . . . . . . . . . . 13 ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}):((1...𝑁) ∪ {(𝑁 + 1)})–1-1-onto→(𝐴 ∪ {𝐵}) → Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
15149, 150syl 17 . . . . . . . . . . . 12 (𝜑 → Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
152 ssun2 3739 . . . . . . . . . . . . 13 {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})
153152a1i 11 . . . . . . . . . . . 12 (𝜑 → {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}))
154 snidg 4153 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℕ0 → (𝑁 + 1) ∈ {(𝑁 + 1)})
15537, 154syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ {(𝑁 + 1)})
156 dmsnopg 5524 . . . . . . . . . . . . . 14 (𝐵 ∈ V → dom {⟨(𝑁 + 1), 𝐵⟩} = {(𝑁 + 1)})
1572, 156syl 17 . . . . . . . . . . . . 13 (𝜑 → dom {⟨(𝑁 + 1), 𝐵⟩} = {(𝑁 + 1)})
158155, 157eleqtrrd 2691 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐵⟩})
159 funssfv 6119 . . . . . . . . . . . 12 ((Fun (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}) ∧ {⟨(𝑁 + 1), 𝐵⟩} ⊆ (𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩}) ∧ (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐵⟩}) → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
160151, 153, 158, 159syl3anc 1318 . . . . . . . . . . 11 (𝜑 → ((𝐺 ∪ {⟨(𝑁 + 1), 𝐵⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
161149, 160syl5eq 2656 . . . . . . . . . 10 (𝜑 → (𝐻‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)))
162 fvsng 6352 . . . . . . . . . . 11 (((𝑁 + 1) ∈ ℕ0𝐵 ∈ V) → ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)) = 𝐵)
16337, 2, 162syl2anc 691 . . . . . . . . . 10 (𝜑 → ({⟨(𝑁 + 1), 𝐵⟩}‘(𝑁 + 1)) = 𝐵)
164161, 163eqtrd 2644 . . . . . . . . 9 (𝜑 → (𝐻‘(𝑁 + 1)) = 𝐵)
165164fveq2d 6107 . . . . . . . 8 (𝜑 → (𝐹‘(𝐻‘(𝑁 + 1))) = (𝐹𝐵))
16696recnd 9947 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
167 ax-1cn 9873 . . . . . . . . . . . 12 1 ∈ ℂ
168 pncan 10166 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
169166, 167, 168sylancl 693 . . . . . . . . . . 11 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
170169fveq2d 6107 . . . . . . . . . 10 (𝜑 → (𝑄‘((𝑁 + 1) − 1)) = (𝑄𝑁))
17175fveq1i 6104 . . . . . . . . . . 11 (𝑄𝑁) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁)
17296, 102gtned 10051 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ≠ 𝑁)
173 fvunsn 6350 . . . . . . . . . . . 12 ((𝑁 + 1) ≠ 𝑁 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁) = (𝑃𝑁))
174172, 173syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘𝑁) = (𝑃𝑁))
175171, 174syl5eq 2656 . . . . . . . . . 10 (𝜑 → (𝑄𝑁) = (𝑃𝑁))
176170, 175eqtrd 2644 . . . . . . . . 9 (𝜑 → (𝑄‘((𝑁 + 1) − 1)) = (𝑃𝑁))
17775fveq1i 6104 . . . . . . . . . . 11 (𝑄‘(𝑁 + 1)) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1))
178 ffun 5961 . . . . . . . . . . . . 13 ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}):((0...𝑁) ∪ {(𝑁 + 1)})⟶𝑉 → Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
17974, 178syl 17 . . . . . . . . . . . 12 (𝜑 → Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
180 ssun2 3739 . . . . . . . . . . . . 13 {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
181180a1i 11 . . . . . . . . . . . 12 (𝜑 → {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}))
182 dmsnopg 5524 . . . . . . . . . . . . . 14 (𝐶𝑉 → dom {⟨(𝑁 + 1), 𝐶⟩} = {(𝑁 + 1)})
18330, 182syl 17 . . . . . . . . . . . . 13 (𝜑 → dom {⟨(𝑁 + 1), 𝐶⟩} = {(𝑁 + 1)})
184155, 183eleqtrrd 2691 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐶⟩})
185 funssfv 6119 . . . . . . . . . . . 12 ((Fun (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}) ∧ {⟨(𝑁 + 1), 𝐶⟩} ⊆ (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩}) ∧ (𝑁 + 1) ∈ dom {⟨(𝑁 + 1), 𝐶⟩}) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
186179, 181, 184, 185syl3anc 1318 . . . . . . . . . . 11 (𝜑 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
187177, 186syl5eq 2656 . . . . . . . . . 10 (𝜑 → (𝑄‘(𝑁 + 1)) = ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)))
188 fvsng 6352 . . . . . . . . . . 11 (((𝑁 + 1) ∈ ℕ0𝐶𝑉) → ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)) = 𝐶)
18937, 30, 188syl2anc 691 . . . . . . . . . 10 (𝜑 → ({⟨(𝑁 + 1), 𝐶⟩}‘(𝑁 + 1)) = 𝐶)
190187, 189eqtrd 2644 . . . . . . . . 9 (𝜑 → (𝑄‘(𝑁 + 1)) = 𝐶)
191176, 190preq12d 4220 . . . . . . . 8 (𝜑 → {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))} = {(𝑃𝑁), 𝐶})
192148, 165, 1913eqtr4d 2654 . . . . . . 7 (𝜑 → (𝐹‘(𝐻‘(𝑁 + 1))) = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))})
193 elsni 4142 . . . . . . . . . 10 (𝑘 ∈ {(𝑁 + 1)} → 𝑘 = (𝑁 + 1))
194193fveq2d 6107 . . . . . . . . 9 (𝑘 ∈ {(𝑁 + 1)} → (𝐻𝑘) = (𝐻‘(𝑁 + 1)))
195194fveq2d 6107 . . . . . . . 8 (𝑘 ∈ {(𝑁 + 1)} → (𝐹‘(𝐻𝑘)) = (𝐹‘(𝐻‘(𝑁 + 1))))
196193oveq1d 6564 . . . . . . . . . 10 (𝑘 ∈ {(𝑁 + 1)} → (𝑘 − 1) = ((𝑁 + 1) − 1))
197196fveq2d 6107 . . . . . . . . 9 (𝑘 ∈ {(𝑁 + 1)} → (𝑄‘(𝑘 − 1)) = (𝑄‘((𝑁 + 1) − 1)))
198193fveq2d 6107 . . . . . . . . 9 (𝑘 ∈ {(𝑁 + 1)} → (𝑄𝑘) = (𝑄‘(𝑁 + 1)))
199197, 198preq12d 4220 . . . . . . . 8 (𝑘 ∈ {(𝑁 + 1)} → {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))})
200195, 199eqeq12d 2625 . . . . . . 7 (𝑘 ∈ {(𝑁 + 1)} → ((𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} ↔ (𝐹‘(𝐻‘(𝑁 + 1))) = {(𝑄‘((𝑁 + 1) − 1)), (𝑄‘(𝑁 + 1))}))
201192, 200syl5ibrcom 236 . . . . . 6 (𝜑 → (𝑘 ∈ {(𝑁 + 1)} → (𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))
202201ralrimiv 2948 . . . . 5 (𝜑 → ∀𝑘 ∈ {(𝑁 + 1)} (𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})
203 ralun 3757 . . . . 5 ((∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} ∧ ∀𝑘 ∈ {(𝑁 + 1)} (𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}) → ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})
204131, 202, 203syl2anc 691 . . . 4 (𝜑 → ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})
20559raleqdv 3121 . . . 4 (𝜑 → (∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} ↔ ∀𝑘 ∈ ((1...𝑁) ∪ {(𝑁 + 1)})(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))
206204, 205mpbird 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→(𝐴 ∪ {𝐵})))
209207, 208syl 17 . . . . 5 (𝑛 = (𝑁 + 1) → (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ↔ 𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵})))
210 oveq2 6557 . . . . . 6 (𝑛 = (𝑁 + 1) → (0...𝑛) = (0...(𝑁 + 1)))
211210feq2d 5944 . . . . 5 (𝑛 = (𝑁 + 1) → (𝑄:(0...𝑛)⟶𝑉𝑄:(0...(𝑁 + 1))⟶𝑉))
212207raleqdv 3121 . . . . 5 (𝑛 = (𝑁 + 1) → (∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)} ↔ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))
213209, 211, 2123anbi123d 1391 . . . 4 (𝑛 = (𝑁 + 1) → ((𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}) ↔ (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...(𝑁 + 1))⟶𝑉 ∧ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})))
214213rspcev 3282 . . 3 (((𝑁 + 1) ∈ ℕ0 ∧ (𝐻:(1...(𝑁 + 1))–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...(𝑁 + 1))⟶𝑉 ∧ ∀𝑘 ∈ (1...(𝑁 + 1))(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)})) → ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))
21537, 62, 80, 206, 214syl13anc 1320 . 2 (𝜑 → ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))
21634fneq1i 5899 . . . . 5 (𝐹 Fn (𝐴 ∪ {𝐵}) ↔ (𝐸 ∪ {⟨𝐵, {(𝑃𝑁), 𝐶}⟩}) Fn (𝐴 ∪ {𝐵}))
217134, 216sylibr 223 . . . 4 (𝜑𝐹 Fn (𝐴 ∪ {𝐵}))
218 fndm 5904 . . . 4 (𝐹 Fn (𝐴 ∪ {𝐵}) → dom 𝐹 = (𝐴 ∪ {𝐵}))
219217, 218syl 17 . . 3 (𝜑 → dom 𝐹 = (𝐴 ∪ {𝐵}))
220 iseupa 26492 . . 3 (dom 𝐹 = (𝐴 ∪ {𝐵}) → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))))
221219, 220syl 17 . 2 (𝜑 → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐴 ∪ {𝐵}) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄𝑘)}))))
22235, 215, 221mpbir2and 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  ℕ0cn0 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)
 Copyright terms: Public domain W3C validator