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

Theorem iseupa 26492
 Description: The property "⟨𝐹, 𝑃⟩ is an Eulerian path on the graph ⟨𝑉, 𝐸⟩". An Eulerian path is defined as bijection 𝐹 from the edges to a set 1...𝑁 a function 𝑃:(0...𝑁)⟶𝑉 into the vertices such that for each 1 ≤ 𝑘 ≤ 𝑁, 𝐹(𝑘) is an edge from 𝑃(𝑘 − 1) to 𝑃(𝑘). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)
Assertion
Ref Expression
iseupa (dom 𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐸,𝑛   𝑘,𝐹,𝑛   𝑃,𝑘,𝑛   𝑘,𝑉,𝑛

Proof of Theorem iseupa
Dummy variables 𝑒 𝑓 𝑝 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-eupa 26490 . . . 4 EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
21brovmpt2ex 7236 . . 3 (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
32a1i 11 . 2 (dom 𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
4 relumgra 25843 . . . . 5 Rel UMGrph
5 brrelex12 5079 . . . . 5 ((Rel UMGrph ∧ 𝑉 UMGrph 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V))
64, 5mpan 702 . . . 4 (𝑉 UMGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))
7 f1of 6050 . . . . . . . 8 (𝐹:(1...𝑛)–1-1-onto𝐴𝐹:(1...𝑛)⟶𝐴)
8 ovex 6577 . . . . . . . 8 (1...𝑛) ∈ V
9 fex 6394 . . . . . . . 8 ((𝐹:(1...𝑛)⟶𝐴 ∧ (1...𝑛) ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 693 . . . . . . 7 (𝐹:(1...𝑛)–1-1-onto𝐴𝐹 ∈ V)
11 ovex 6577 . . . . . . . 8 (0...𝑛) ∈ V
12 fex 6394 . . . . . . . 8 ((𝑃:(0...𝑛)⟶𝑉 ∧ (0...𝑛) ∈ V) → 𝑃 ∈ V)
1311, 12mpan2 703 . . . . . . 7 (𝑃:(0...𝑛)⟶𝑉𝑃 ∈ V)
1410, 13anim12i 588 . . . . . 6 ((𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉) → (𝐹 ∈ V ∧ 𝑃 ∈ V))
15143adant3 1074 . . . . 5 ((𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}) → (𝐹 ∈ V ∧ 𝑃 ∈ V))
1615rexlimivw 3011 . . . 4 (∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}) → (𝐹 ∈ V ∧ 𝑃 ∈ V))
176, 16anim12i 588 . . 3 ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
1817a1i 11 . 2 (dom 𝐸 = 𝐴 → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))))
191a1i 11 . . . . . 6 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}))
20 breq12 4588 . . . . . . . . 9 ((𝑣 = 𝑉𝑒 = 𝐸) → (𝑣 UMGrph 𝑒𝑉 UMGrph 𝐸))
2120adantl 481 . . . . . . . 8 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (𝑣 UMGrph 𝑒𝑉 UMGrph 𝐸))
22 simprr 792 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → 𝑒 = 𝐸)
2322dmeqd 5248 . . . . . . . . . . . 12 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → dom 𝑒 = dom 𝐸)
24 simplr 788 . . . . . . . . . . . 12 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → dom 𝐸 = 𝐴)
2523, 24eqtrd 2644 . . . . . . . . . . 11 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → dom 𝑒 = 𝐴)
2625f1oeq3d 6047 . . . . . . . . . 10 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑓:(1...𝑛)–1-1-onto𝐴))
27 feq3 5941 . . . . . . . . . . 11 (𝑣 = 𝑉 → (𝑝:(0...𝑛)⟶𝑣𝑝:(0...𝑛)⟶𝑉))
2827ad2antrl 760 . . . . . . . . . 10 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (𝑝:(0...𝑛)⟶𝑣𝑝:(0...𝑛)⟶𝑉))
2922fveq1d 6105 . . . . . . . . . . . 12 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (𝑒‘(𝑓𝑘)) = (𝐸‘(𝑓𝑘)))
3029eqeq1d 2612 . . . . . . . . . . 11 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → ((𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)} ↔ (𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))
3130ralbidv 2969 . . . . . . . . . 10 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)} ↔ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))
3226, 28, 313anbi123d 1391 . . . . . . . . 9 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → ((𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) ↔ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})))
3332rexbidv 3034 . . . . . . . 8 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) ↔ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})))
3421, 33anbi12d 743 . . . . . . 7 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → ((𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))))
3534opabbidv 4648 . . . . . 6 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉𝑒 = 𝐸)) → {⟨𝑓, 𝑝⟩ ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} = {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
36 simplll 794 . . . . . 6 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → 𝑉 ∈ V)
37 simpllr 795 . . . . . 6 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → 𝐸 ∈ V)
38 simpr 476 . . . . . . . . . . . . . . 15 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → dom 𝐸 = 𝐴)
39 dmexg 6989 . . . . . . . . . . . . . . . 16 (𝐸 ∈ V → dom 𝐸 ∈ V)
4037, 39syl 17 . . . . . . . . . . . . . . 15 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → dom 𝐸 ∈ V)
4138, 40eqeltrrd 2689 . . . . . . . . . . . . . 14 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → 𝐴 ∈ V)
4241adantr 480 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝐴 ∈ V)
43 nnex 10903 . . . . . . . . . . . . . 14 ℕ ∈ V
4443a1i 11 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → ℕ ∈ V)
45 simpr1 1060 . . . . . . . . . . . . . 14 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑓:(1...𝑛)–1-1-onto𝐴)
46 f1of 6050 . . . . . . . . . . . . . 14 (𝑓:(1...𝑛)–1-1-onto𝐴𝑓:(1...𝑛)⟶𝐴)
4745, 46syl 17 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑓:(1...𝑛)⟶𝐴)
48 fz1ssnn 12243 . . . . . . . . . . . . . 14 (1...𝑛) ⊆ ℕ
4948a1i 11 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → (1...𝑛) ⊆ ℕ)
50 elpm2r 7761 . . . . . . . . . . . . 13 (((𝐴 ∈ V ∧ ℕ ∈ V) ∧ (𝑓:(1...𝑛)⟶𝐴 ∧ (1...𝑛) ⊆ ℕ)) → 𝑓 ∈ (𝐴pm ℕ))
5142, 44, 47, 49, 50syl22anc 1319 . . . . . . . . . . . 12 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑓 ∈ (𝐴pm ℕ))
5236adantr 480 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑉 ∈ V)
53 nn0ex 11175 . . . . . . . . . . . . . 14 0 ∈ V
5453a1i 11 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → ℕ0 ∈ V)
55 simpr2 1061 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑝:(0...𝑛)⟶𝑉)
56 fz0ssnn0 12304 . . . . . . . . . . . . . 14 (0...𝑛) ⊆ ℕ0
5756a1i 11 . . . . . . . . . . . . 13 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → (0...𝑛) ⊆ ℕ0)
58 elpm2r 7761 . . . . . . . . . . . . 13 (((𝑉 ∈ V ∧ ℕ0 ∈ V) ∧ (𝑝:(0...𝑛)⟶𝑉 ∧ (0...𝑛) ⊆ ℕ0)) → 𝑝 ∈ (𝑉pm0))
5952, 54, 55, 57, 58syl22anc 1319 . . . . . . . . . . . 12 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → 𝑝 ∈ (𝑉pm0))
6051, 59jca 553 . . . . . . . . . . 11 (((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0)))
6160ex 449 . . . . . . . . . 10 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → ((𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) → (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))))
6261rexlimdvw 3016 . . . . . . . . 9 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) → (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))))
6362adantld 482 . . . . . . . 8 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) → (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))))
6463ssopab2dv 4929 . . . . . . 7 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} ⊆ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))})
65 df-xp 5044 . . . . . . . 8 ((𝐴pm ℕ) × (𝑉pm0)) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))}
66 ovex 6577 . . . . . . . . 9 (𝐴pm ℕ) ∈ V
67 ovex 6577 . . . . . . . . 9 (𝑉pm0) ∈ V
6866, 67xpex 6860 . . . . . . . 8 ((𝐴pm ℕ) × (𝑉pm0)) ∈ V
6965, 68eqeltrri 2685 . . . . . . 7 {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))} ∈ V
70 ssexg 4732 . . . . . . 7 (({⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} ⊆ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))} ∧ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ (𝐴pm ℕ) ∧ 𝑝 ∈ (𝑉pm0))} ∈ V) → {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} ∈ V)
7164, 69, 70sylancl 693 . . . . . 6 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} ∈ V)
7219, 35, 36, 37, 71ovmpt2d 6686 . . . . 5 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝑉 EulPaths 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))})
7372breqd 4594 . . . 4 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝐹(𝑉 EulPaths 𝐸)𝑃𝐹{⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}𝑃))
74 f1oeq1 6040 . . . . . . . . . 10 (𝑓 = 𝐹 → (𝑓:(1...𝑛)–1-1-onto𝐴𝐹:(1...𝑛)–1-1-onto𝐴))
7574adantr 480 . . . . . . . . 9 ((𝑓 = 𝐹𝑝 = 𝑃) → (𝑓:(1...𝑛)–1-1-onto𝐴𝐹:(1...𝑛)–1-1-onto𝐴))
76 feq1 5939 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝:(0...𝑛)⟶𝑉𝑃:(0...𝑛)⟶𝑉))
7776adantl 481 . . . . . . . . 9 ((𝑓 = 𝐹𝑝 = 𝑃) → (𝑝:(0...𝑛)⟶𝑉𝑃:(0...𝑛)⟶𝑉))
78 fveq1 6102 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (𝑓𝑘) = (𝐹𝑘))
7978fveq2d 6107 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝐸‘(𝑓𝑘)) = (𝐸‘(𝐹𝑘)))
8079adantr 480 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑝 = 𝑃) → (𝐸‘(𝑓𝑘)) = (𝐸‘(𝐹𝑘)))
81 simpr 476 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑝 = 𝑃) → 𝑝 = 𝑃)
8281fveq1d 6105 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑝 = 𝑃) → (𝑝‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1)))
8381fveq1d 6105 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑝 = 𝑃) → (𝑝𝑘) = (𝑃𝑘))
8482, 83preq12d 4220 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑝 = 𝑃) → {(𝑝‘(𝑘 − 1)), (𝑝𝑘)} = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})
8580, 84eqeq12d 2625 . . . . . . . . . 10 ((𝑓 = 𝐹𝑝 = 𝑃) → ((𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)} ↔ (𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))
8685ralbidv 2969 . . . . . . . . 9 ((𝑓 = 𝐹𝑝 = 𝑃) → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)} ↔ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))
8775, 77, 863anbi123d 1391 . . . . . . . 8 ((𝑓 = 𝐹𝑝 = 𝑃) → ((𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) ↔ (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})))
8887rexbidv 3034 . . . . . . 7 ((𝑓 = 𝐹𝑝 = 𝑃) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}) ↔ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})))
8988anbi2d 736 . . . . . 6 ((𝑓 = 𝐹𝑝 = 𝑃) → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)})) ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
90 eqid 2610 . . . . . 6 {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))} = {⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}
9189, 90brabga 4914 . . . . 5 ((𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹{⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
9291ad2antlr 759 . . . 4 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝐹{⟨𝑓, 𝑝⟩ ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto𝐴𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝𝑘)}))}𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
9373, 92bitrd 267 . . 3 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
9493expcom 450 . 2 (dom 𝐸 = 𝐴 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)})))))
953, 18, 94pm5.21ndd 368 1 (dom 𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto𝐴𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃𝑘)}))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  {cpr 4127   class class class wbr 4583  {copab 4642   × cxp 5036  dom cdm 5038  Rel wrel 5043  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑pm cpm 7745  0cc0 9815  1c1 9816   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  ...cfz 12197   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-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-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-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  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-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-umgra 25842  df-eupa 26490 This theorem is referenced by:  eupagra  26493  eupai  26494  eupatrl  26495  eupa0  26501  eupares  26502  eupap1  26503
 Copyright terms: Public domain W3C validator