Proof of Theorem 2wlklem1
Step | Hyp | Ref
| Expression |
1 | | simprl 790 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘𝐼) = {𝐴, 𝐵}) |
2 | | 2trlY.f |
. . . . 5
⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} |
3 | | fveq1 6102 |
. . . . . 6
⊢ (𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} → (𝐹‘0) = ({〈0, 𝐼〉, 〈1, 𝐽〉}‘0)) |
4 | | 0ne1 10965 |
. . . . . . 7
⊢ 0 ≠
1 |
5 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
6 | | 2trlY.i |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) |
7 | | elex 3185 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑈 → 𝐼 ∈ V) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) → 𝐼 ∈ V) |
9 | 6, 8 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐼 ∈ V |
10 | 5, 9 | fvpr1 6361 |
. . . . . . 7
⊢ (0 ≠ 1
→ ({〈0, 𝐼〉,
〈1, 𝐽〉}‘0)
= 𝐼) |
11 | 4, 10 | ax-mp 5 |
. . . . . 6
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}‘0)
= 𝐼 |
12 | 3, 11 | syl6eq 2660 |
. . . . 5
⊢ (𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} → (𝐹‘0) = 𝐼) |
13 | 2, 12 | mp1i 13 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐹‘0) = 𝐼) |
14 | 13 | fveq2d 6107 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘(𝐹‘0)) = (𝐸‘𝐼)) |
15 | | 2trlY.p |
. . . . . . 7
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
16 | 15 | 2wlklemA 26084 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) |
17 | 16 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘0) = 𝐴) |
18 | 17 | ad2antlr 759 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝑃‘0) = 𝐴) |
19 | 15 | 2wlklemB 26085 |
. . . . . 6
⊢ (𝐵 ∈ 𝑉 → (𝑃‘1) = 𝐵) |
20 | 19 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘1) = 𝐵) |
21 | 20 | ad2antlr 759 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝑃‘1) = 𝐵) |
22 | 18, 21 | preq12d 4220 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) |
23 | 1, 14, 22 | 3eqtr4d 2654 |
. 2
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
24 | | simprr 792 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘𝐽) = {𝐵, 𝐶}) |
25 | | fveq1 6102 |
. . . . . 6
⊢ (𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} → (𝐹‘1) = ({〈0, 𝐼〉, 〈1, 𝐽〉}‘1)) |
26 | | 1ex 9914 |
. . . . . . . 8
⊢ 1 ∈
V |
27 | | elex 3185 |
. . . . . . . . . 10
⊢ (𝐽 ∈ 𝑊 → 𝐽 ∈ V) |
28 | 27 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) → 𝐽 ∈ V) |
29 | 6, 28 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐽 ∈ V |
30 | 26, 29 | fvpr2 6362 |
. . . . . . 7
⊢ (0 ≠ 1
→ ({〈0, 𝐼〉,
〈1, 𝐽〉}‘1)
= 𝐽) |
31 | 4, 30 | ax-mp 5 |
. . . . . 6
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}‘1)
= 𝐽 |
32 | 25, 31 | syl6eq 2660 |
. . . . 5
⊢ (𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} → (𝐹‘1) = 𝐽) |
33 | 2, 32 | mp1i 13 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐹‘1) = 𝐽) |
34 | 33 | fveq2d 6107 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘(𝐹‘1)) = (𝐸‘𝐽)) |
35 | 15 | 2wlklemC 26086 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → (𝑃‘2) = 𝐶) |
36 | 35 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘2) = 𝐶) |
37 | 36 | ad2antlr 759 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝑃‘2) = 𝐶) |
38 | 21, 37 | preq12d 4220 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {(𝑃‘1), (𝑃‘2)} = {𝐵, 𝐶}) |
39 | 24, 34, 38 | 3eqtr4d 2654 |
. 2
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) |
40 | | 2wlklem 26094 |
. 2
⊢
(∀𝑘 ∈
{0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
41 | 23, 39, 40 | sylanbrc 695 |
1
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |