Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . 3
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝑉 ∈ V) |
3 | | elex 3185 |
. . 3
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
4 | 3 | adantl 481 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ∈ V) |
5 | | 3xpexg 6859 |
. . . 4
⊢ (𝑉 ∈ 𝑋 → ((𝑉 × 𝑉) × 𝑉) ∈ V) |
6 | 5 | adantr 480 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 × 𝑉) × 𝑉) ∈ V) |
7 | | rabexg 4739 |
. . 3
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ∈ V) |
8 | 6, 7 | syl 17 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ∈ V) |
9 | | id 22 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉) |
10 | 9, 9 | xpeq12d 5064 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (𝑣 × 𝑣) = (𝑉 × 𝑉)) |
11 | 10, 9 | xpeq12d 5064 |
. . . . 5
⊢ (𝑣 = 𝑉 → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉)) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉)) |
13 | | simpl 472 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
14 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 2WalksOnOt 𝑒) = (𝑉 2WalksOnOt 𝐸)) |
15 | 14 | oveqd 6566 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎(𝑣 2WalksOnOt 𝑒)𝑏) = (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)) |
16 | 15 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏) ↔ 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
17 | 13, 16 | rexeqbidv 3130 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏) ↔ ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
18 | 13, 17 | rexeqbidv 3130 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
19 | 12, 18 | rabeqbidv 3168 |
. . 3
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) |
20 | | df-2wlksot 26386 |
. . 3
⊢ 2WalksOt
= (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)}) |
21 | 19, 20 | ovmpt2ga 6688 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ∈ V) → (𝑉 2WalksOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) |
22 | 2, 4, 8, 21 | syl3anc 1318 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2WalksOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) |