Step | Hyp | Ref
| Expression |
1 | | df-eupa 26490 |
. . . 4
⊢ EulPaths
= (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom
𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}) |
2 | 1 | brovmpt2ex 7236 |
. . 3
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | 2 | a1i 11 |
. 2
⊢ (dom
𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
4 | | relumgra 25843 |
. . . . 5
⊢ Rel
UMGrph |
5 | | brrelex12 5079 |
. . . . 5
⊢ ((Rel
UMGrph ∧ 𝑉 UMGrph 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
6 | 4, 5 | mpan 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) |
10 | 7, 8, 9 | sylancl 693 |
. . . . . . 7
⊢ (𝐹:(1...𝑛)–1-1-onto→𝐴 → 𝐹 ∈ V) |
11 | | ovex 6577 |
. . . . . . . 8
⊢
(0...𝑛) ∈
V |
12 | | fex 6394 |
. . . . . . . 8
⊢ ((𝑃:(0...𝑛)⟶𝑉 ∧ (0...𝑛) ∈ V) → 𝑃 ∈ V) |
13 | 11, 12 | mpan2 703 |
. . . . . . 7
⊢ (𝑃:(0...𝑛)⟶𝑉 → 𝑃 ∈ V) |
14 | 10, 13 | anim12i 588 |
. . . . . 6
⊢ ((𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
15 | 14 | 3adant3 1074 |
. . . . 5
⊢ ((𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
16 | 15 | rexlimivw 3011 |
. . . 4
⊢
(∃𝑛 ∈
ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
17 | 6, 16 | anim12i 588 |
. . 3
⊢ ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
18 | 17 | a1i 11 |
. 2
⊢ (dom
𝐸 = 𝐴 → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))) |
19 | 1 | a1i 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 𝐸)) |
21 | 20 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑣 UMGrph 𝑒 ↔ 𝑉 UMGrph 𝐸)) |
22 | | simprr 792 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → 𝑒 = 𝐸) |
23 | 22 | dmeqd 5248 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝑒 = dom 𝐸) |
24 | | simplr 788 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝐸 = 𝐴) |
25 | 23, 24 | eqtrd 2644 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝑒 = 𝐴) |
26 | 25 | f1oeq3d 6047 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑓:(1...𝑛)–1-1-onto→dom
𝑒 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴)) |
27 | | feq3 5941 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑉 → (𝑝:(0...𝑛)⟶𝑣 ↔ 𝑝:(0...𝑛)⟶𝑉)) |
28 | 27 | ad2antrl 760 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑝:(0...𝑛)⟶𝑣 ↔ 𝑝:(0...𝑛)⟶𝑉)) |
29 | 22 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑒‘(𝑓‘𝑘)) = (𝐸‘(𝑓‘𝑘))) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → ((𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)} ↔ (𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) |
31 | 30 | ralbidv 2969 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)} ↔ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) |
32 | 26, 28, 31 | 3anbi123d 1391 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → ((𝑓:(1...𝑛)–1-1-onto→dom
𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) ↔ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))) |
33 | 32 | rexbidv 3034 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom
𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) ↔ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))) |
34 | 21, 33 | anbi12d 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)), (𝑝‘𝑘)})))) |
35 | 34 | opabbidv 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) |
40 | 37, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → dom 𝐸 ∈ V) |
41 | 38, 40 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → 𝐴 ∈ V) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → 𝐴 ∈ V) |
43 | | nnex 10903 |
. . . . . . . . . . . . . 14
⊢ ℕ
∈ V |
44 | 43 | a1i 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...𝑛)⟶𝐴) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → 𝑓:(1...𝑛)⟶𝐴) |
48 | | fz1ssnn 12243 |
. . . . . . . . . . . . . 14
⊢
(1...𝑛) ⊆
ℕ |
49 | 48 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → (1...𝑛) ⊆ ℕ) |
50 | | elpm2r 7761 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ V ∧ ℕ ∈
V) ∧ (𝑓:(1...𝑛)⟶𝐴 ∧ (1...𝑛) ⊆ ℕ)) → 𝑓 ∈ (𝐴 ↑pm
ℕ)) |
51 | 42, 44, 47, 49, 50 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → 𝑓 ∈ (𝐴 ↑pm
ℕ)) |
52 | 36 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → 𝑉 ∈ V) |
53 | | nn0ex 11175 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
54 | 53 | a1i 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 |
57 | 56 | a1i 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)) → 𝑝 ∈ (𝑉 ↑pm
ℕ0)) |
59 | 52, 54, 55, 57, 58 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → 𝑝 ∈ (𝑉 ↑pm
ℕ0)) |
60 | 51, 59 | jca 553 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) ∧ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))) |
61 | 60 | ex 449 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) → (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0)))) |
62 | 61 | rexlimdvw 3016 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) → (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0)))) |
63 | 62 | adantld 482 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)})) → (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0)))) |
64 | 63 | ssopab2dv 4929 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → {〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))} ⊆ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))}) |
65 | | df-xp 5044 |
. . . . . . . 8
⊢ ((𝐴 ↑pm
ℕ) × (𝑉
↑pm ℕ0)) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))} |
66 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐴 ↑pm
ℕ) ∈ V |
67 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑉 ↑pm
ℕ0) ∈ V |
68 | 66, 67 | xpex 6860 |
. . . . . . . 8
⊢ ((𝐴 ↑pm
ℕ) × (𝑉
↑pm ℕ0)) ∈ V |
69 | 65, 68 | eqeltrri 2685 |
. . . . . . 7
⊢
{〈𝑓, 𝑝〉 ∣ (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))} ∈ V |
70 | | ssexg 4732 |
. . . . . . 7
⊢
(({〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))} ⊆ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))} ∧ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ (𝐴 ↑pm ℕ) ∧
𝑝 ∈ (𝑉 ↑pm
ℕ0))} ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))} ∈ V) |
71 | 64, 69, 70 | sylancl 693 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → {〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))} ∈ V) |
72 | 19, 35, 36, 37, 71 | ovmpt2d 6686 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝑉 EulPaths 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}) |
73 | 72 | breqd 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→𝐴)) |
75 | 74 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑓:(1...𝑛)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑛)–1-1-onto→𝐴)) |
76 | | feq1 5939 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝:(0...𝑛)⟶𝑉 ↔ 𝑃:(0...𝑛)⟶𝑉)) |
77 | 76 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝:(0...𝑛)⟶𝑉 ↔ 𝑃:(0...𝑛)⟶𝑉)) |
78 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → (𝑓‘𝑘) = (𝐹‘𝑘)) |
79 | 78 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (𝐸‘(𝑓‘𝑘)) = (𝐸‘(𝐹‘𝑘))) |
80 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝐸‘(𝑓‘𝑘)) = (𝐸‘(𝐹‘𝑘))) |
81 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
82 | 81 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1))) |
83 | 81 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝑝‘𝑘) = (𝑃‘𝑘)) |
84 | 82, 83 | preq12d 4220 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)} = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) |
85 | 80, 84 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)} ↔ (𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
86 | 85 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)} ↔ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
87 | 75, 77, 86 | 3anbi123d 1391 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) ↔ (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
88 | 87 | rexbidv 3034 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}) ↔ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
89 | 88 | anbi2d 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)), (𝑝‘𝑘)}))} |
91 | 89, 90 | brabga 4914 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹{〈𝑓, 𝑝〉 ∣ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑝:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
92 | 91 | ad2antlr 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)), (𝑃‘𝑘)})))) |
93 | 73, 92 | bitrd 267 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ dom 𝐸 = 𝐴) → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
94 | 93 | expcom 450 |
. 2
⊢ (dom
𝐸 = 𝐴 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))))) |
95 | 3, 18, 94 | pm5.21ndd 368 |
1
⊢ (dom
𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |