Step | Hyp | Ref
| Expression |
1 | | 1trl.f |
. . 3
⊢ 𝐹 = {〈0, 𝑖〉} |
2 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
3 | | vex 3176 |
. . . . . . 7
⊢ 𝑖 ∈ V |
4 | 2, 3 | f1osn 6088 |
. . . . . 6
⊢ {〈0,
𝑖〉}:{0}–1-1-onto→{𝑖} |
5 | | f1of1 6049 |
. . . . . 6
⊢
({〈0, 𝑖〉}:{0}–1-1-onto→{𝑖} → {〈0, 𝑖〉}:{0}–1-1→{𝑖}) |
6 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 = {〈0, 𝑖〉} → (#‘𝐹) = (#‘{〈0, 𝑖〉})) |
7 | | opex 4859 |
. . . . . . . . . . . . . . . . 17
⊢ 〈0,
𝑖〉 ∈
V |
8 | | hashsng 13020 |
. . . . . . . . . . . . . . . . 17
⊢ (〈0,
𝑖〉 ∈ V →
(#‘{〈0, 𝑖〉}) = 1) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(#‘{〈0, 𝑖〉}) = 1 |
10 | 6, 9 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = {〈0, 𝑖〉} → (#‘𝐹) = 1) |
11 | 1, 10 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(#‘𝐹) =
1 |
12 | 11 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢
(0..^(#‘𝐹)) =
(0..^1) |
13 | | fzo01 12417 |
. . . . . . . . . . . . 13
⊢ (0..^1) =
{0} |
14 | 12, 13 | eqtri 2632 |
. . . . . . . . . . . 12
⊢
(0..^(#‘𝐹)) =
{0} |
15 | 14 | eqcomi 2619 |
. . . . . . . . . . 11
⊢ {0} =
(0..^(#‘𝐹)) |
16 | | f1eq2 6010 |
. . . . . . . . . . 11
⊢ ({0} =
(0..^(#‘𝐹)) →
({〈0, 𝑖〉}:{0}–1-1→{𝑖} ↔ {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→{𝑖})) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
⊢
({〈0, 𝑖〉}:{0}–1-1→{𝑖} ↔ {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→{𝑖}) |
18 | 17 | biimpi 205 |
. . . . . . . . 9
⊢
({〈0, 𝑖〉}:{0}–1-1→{𝑖} → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→{𝑖}) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→{𝑖}) |
20 | | prid1g 4239 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵}) |
22 | 21 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵}) |
23 | 22 | adantl 481 |
. . . . . . . . . . 11
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → 𝐴 ∈ {𝐴, 𝐵}) |
24 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ ((𝐸‘𝑖) = {𝐴, 𝐵} → (𝐴 ∈ (𝐸‘𝑖) ↔ 𝐴 ∈ {𝐴, 𝐵})) |
25 | 24 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐴 ∈ (𝐸‘𝑖) ↔ 𝐴 ∈ {𝐴, 𝐵})) |
26 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → (𝐴 ∈ (𝐸‘𝑖) ↔ 𝐴 ∈ {𝐴, 𝐵})) |
27 | 23, 26 | mpbird 246 |
. . . . . . . . . 10
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → 𝐴 ∈ (𝐸‘𝑖)) |
28 | | elfvdm 6130 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝐸‘𝑖) → 𝑖 ∈ dom 𝐸) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → 𝑖 ∈ dom 𝐸) |
30 | 29 | snssd 4281 |
. . . . . . . 8
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → {𝑖} ⊆ dom 𝐸) |
31 | | f1ss 6019 |
. . . . . . . 8
⊢
(({〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→{𝑖} ∧ {𝑖} ⊆ dom 𝐸) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
32 | 19, 30, 31 | syl2anc 691 |
. . . . . . 7
⊢
(({〈0, 𝑖〉}:{0}–1-1→{𝑖} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
33 | 32 | ex 449 |
. . . . . 6
⊢
({〈0, 𝑖〉}:{0}–1-1→{𝑖} → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
34 | 4, 5, 33 | mp2b 10 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
35 | 34 | adantl 481 |
. . . 4
⊢ ((𝐹 = {〈0, 𝑖〉} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
36 | | f1eq1 6009 |
. . . . 5
⊢ (𝐹 = {〈0, 𝑖〉} → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
37 | 36 | adantr 480 |
. . . 4
⊢ ((𝐹 = {〈0, 𝑖〉} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ {〈0, 𝑖〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
38 | 35, 37 | mpbird 246 |
. . 3
⊢ ((𝐹 = {〈0, 𝑖〉} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵})) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) |
39 | 1, 38 | mpan 702 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) |
40 | | 1trl.p |
. . . 4
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} |
41 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
42 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
43 | 41, 42 | pm3.2i 470 |
. . . . . . . 8
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
44 | | 0ne1 10965 |
. . . . . . . 8
⊢ 0 ≠
1 |
45 | | fprg 6327 |
. . . . . . . . 9
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}⟶{𝐴, 𝐵}) |
46 | | 0p1e1 11009 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
47 | 46 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ 1 = (0 +
1) |
48 | 47 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (0...1) =
(0...(0 + 1)) |
49 | | fzpr 12266 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
50 | 41, 49 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
51 | 46 | preq2i 4216 |
. . . . . . . . . . 11
⊢ {0, (0 +
1)} = {0, 1} |
52 | 48, 50, 51 | 3eqtri 2636 |
. . . . . . . . . 10
⊢ (0...1) =
{0, 1} |
53 | 52 | feq2i 5950 |
. . . . . . . . 9
⊢
({〈0, 𝐴〉,
〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵} ↔ {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}⟶{𝐴, 𝐵}) |
54 | 45, 53 | sylibr 223 |
. . . . . . . 8
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵}) |
55 | 43, 44, 54 | mp3an13 1407 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵}) |
56 | | prssi 4293 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ⊆ 𝑉) |
57 | 55, 56 | fssd 5970 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉) |
58 | 57 | adantl 481 |
. . . . 5
⊢ ((𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉) |
59 | | id 22 |
. . . . . . 7
⊢ (𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} → 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉}) |
60 | 11 | oveq2i 6560 |
. . . . . . . 8
⊢
(0...(#‘𝐹)) =
(0...1) |
61 | 60 | a1i 11 |
. . . . . . 7
⊢ (𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (0...(#‘𝐹)) = (0...1)) |
62 | 59, 61 | feq12d 5946 |
. . . . . 6
⊢ (𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉)) |
63 | 62 | adantr 480 |
. . . . 5
⊢ ((𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉)) |
64 | 58, 63 | mpbird 246 |
. . . 4
⊢ ((𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
65 | 40, 64 | mpan 702 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
66 | 65 | 3ad2ant2 1076 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
67 | | id 22 |
. . . . . 6
⊢ ((𝐸‘𝑖) = {𝐴, 𝐵} → (𝐸‘𝑖) = {𝐴, 𝐵}) |
68 | 67 | 3ad2ant3 1077 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐸‘𝑖) = {𝐴, 𝐵}) |
69 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝐹 = {〈0, 𝑖〉} → (𝐹‘0) = ({〈0, 𝑖〉}‘0)) |
70 | 2, 3 | fvsn 6351 |
. . . . . . . . 9
⊢
({〈0, 𝑖〉}‘0) = 𝑖 |
71 | 69, 70 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐹 = {〈0, 𝑖〉} → (𝐹‘0) = 𝑖) |
72 | 1, 71 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹‘0) = 𝑖 |
73 | 72 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐹‘0) = 𝑖) |
74 | 73 | fveq2d 6107 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐸‘(𝐹‘0)) = (𝐸‘𝑖)) |
75 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (𝑃‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0)) |
76 | | fvpr1g 6363 |
. . . . . . . . . . 11
⊢ ((0
∈ V ∧ 𝐴 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘0)
= 𝐴) |
77 | 2, 44, 76 | mp3an13 1407 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
78 | 75, 77 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} ∧ 𝐴 ∈ 𝑉) → (𝑃‘0) = 𝐴) |
79 | 40, 78 | mpan 702 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) |
80 | 79 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑃‘0) = 𝐴) |
81 | 80 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝑃‘0) = 𝐴) |
82 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} → (𝑃‘1) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1)) |
83 | | 1ex 9914 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
84 | | fvpr2g 6364 |
. . . . . . . . . . 11
⊢ ((1
∈ V ∧ 𝐵 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘1)
= 𝐵) |
85 | 83, 44, 84 | mp3an13 1407 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1) = 𝐵) |
86 | 82, 85 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉} ∧ 𝐵 ∈ 𝑉) → (𝑃‘1) = 𝐵) |
87 | 40, 86 | mpan 702 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝑃‘1) = 𝐵) |
88 | 87 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑃‘1) = 𝐵) |
89 | 88 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝑃‘1) = 𝐵) |
90 | 81, 89 | preq12d 4220 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) |
91 | 68, 74, 90 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
92 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
93 | 92 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘0))) |
94 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
95 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
96 | 95, 46 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
97 | 96 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
98 | 94, 97 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
99 | 93, 98 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 0 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
100 | 2, 99 | ralsn 4169 |
. . . 4
⊢
(∀𝑘 ∈
{0} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
101 | 91, 100 | sylibr 223 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ∀𝑘 ∈ {0} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
102 | 14 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (0..^(#‘𝐹)) = {0}) |
103 | 102 | raleqdv 3121 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
104 | 101, 103 | mpbird 246 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
105 | | snex 4835 |
. . . . 5
⊢ {〈0,
𝑖〉} ∈
V |
106 | 1, 105 | eqeltri 2684 |
. . . 4
⊢ 𝐹 ∈ V |
107 | | prex 4836 |
. . . . 5
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉} ∈
V |
108 | 40, 107 | eqeltri 2684 |
. . . 4
⊢ 𝑃 ∈ V |
109 | | istrl2 26068 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
110 | 106, 108,
109 | mpanr12 717 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
111 | 110 | 3ad2ant1 1075 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
112 | 39, 66, 104, 111 | mpbir3and 1238 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐹(𝑉 Trails 𝐸)𝑃) |