Step | Hyp | Ref
| Expression |
1 | | 2nn0 11186 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
2 | | wwlks2onv.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 2 | wwlksnon 41049 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ 𝐺 ∈ V) → (2 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})) |
4 | 1, 3 | mpan 702 |
. . . . . . 7
⊢ (𝐺 ∈ V → (2 WWalksNOn
𝐺) = (𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})) |
5 | 4 | oveqd 6566 |
. . . . . 6
⊢ (𝐺 ∈ V → (𝐴(2 WWalksNOn 𝐺)𝐶) = (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶)) |
6 | 5 | eleq2d 2673 |
. . . . 5
⊢ (𝐺 ∈ V →
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶))) |
7 | | eqid 2610 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)}) = (𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)}) |
8 | 7 | elmpt2cl 6774 |
. . . . . 6
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
9 | | simprl 790 |
. . . . . . . 8
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ∧ 𝐵 ∈ 𝑈) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
10 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐴 → ((𝑤‘0) = 𝑎 ↔ (𝑤‘0) = 𝐴)) |
11 | 10 | anbi1d 737 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐴 → (((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐) ↔ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝑐))) |
12 | 11 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)} = {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝑐)}) |
13 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝐶 → ((𝑤‘2) = 𝑐 ↔ (𝑤‘2) = 𝐶)) |
14 | 13 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐶 → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝑐) ↔ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶))) |
15 | 14 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐶 → {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝑐)} = {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)}) |
16 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (2
WWalkSN 𝐺) ∈
V |
17 | 16 | rabex 4740 |
. . . . . . . . . . . . 13
⊢ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)} ∈ V |
18 | 12, 15, 7, 17 | ovmpt2 6694 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) = {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)}) |
19 | 18 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)})) |
20 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
21 | 20 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘0) = 𝐴 ↔ (〈“𝐴𝐵𝐶”〉‘0) = 𝐴)) |
22 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (𝑤‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
23 | 22 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → ((𝑤‘2) = 𝐶 ↔ (〈“𝐴𝐵𝐶”〉‘2) = 𝐶)) |
24 | 21, 23 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈“𝐴𝐵𝐶”〉 → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶) ↔ ((〈“𝐴𝐵𝐶”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝐶”〉‘2) = 𝐶))) |
25 | 24 | elrab 3331 |
. . . . . . . . . . . 12
⊢
(〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)} ↔ (〈“𝐴𝐵𝐶”〉 ∈ (2 WWalkSN 𝐺) ∧ ((〈“𝐴𝐵𝐶”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝐶”〉‘2) = 𝐶))) |
26 | | wwlknbp2 41063 |
. . . . . . . . . . . . . . 15
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (2 WWalkSN 𝐺) → (〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1))) |
27 | | s3fv1 13487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ 𝑈 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
28 | 27 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ 𝑈 → 𝐵 = (〈“𝐴𝐵𝐶”〉‘1)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) ∧ 𝐵 ∈ 𝑈) → 𝐵 = (〈“𝐴𝐵𝐶”〉‘1)) |
30 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
31 | 30 | tpid2 4247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
{0, 1, 2} |
32 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘〈“𝐴𝐵𝐶”〉) = (2 + 1) →
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) |
33 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 + 1) =
3 |
34 | 32, 33 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘〈“𝐴𝐵𝐶”〉) = (2 + 1) →
(#‘〈“𝐴𝐵𝐶”〉) = 3) |
35 | 34 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘〈“𝐴𝐵𝐶”〉) = (2 + 1) →
(0..^(#‘〈“𝐴𝐵𝐶”〉)) = (0..^3)) |
36 | | fzo0to3tp 12421 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0..^3) =
{0, 1, 2} |
37 | 35, 36 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘〈“𝐴𝐵𝐶”〉) = (2 + 1) →
(0..^(#‘〈“𝐴𝐵𝐶”〉)) = {0, 1,
2}) |
38 | 31, 37 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘〈“𝐴𝐵𝐶”〉) = (2 + 1) → 1 ∈
(0..^(#‘〈“𝐴𝐵𝐶”〉))) |
39 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧ 1 ∈
(0..^(#‘〈“𝐴𝐵𝐶”〉))) → (〈“𝐴𝐵𝐶”〉‘1) ∈
(Vtx‘𝐺)) |
40 | 39, 2 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧ 1 ∈
(0..^(#‘〈“𝐴𝐵𝐶”〉))) → (〈“𝐴𝐵𝐶”〉‘1) ∈ 𝑉) |
41 | 38, 40 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) →
(〈“𝐴𝐵𝐶”〉‘1) ∈ 𝑉) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) ∧ 𝐵 ∈ 𝑈) → (〈“𝐴𝐵𝐶”〉‘1) ∈ 𝑉) |
43 | 29, 42 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) ∧ 𝐵 ∈ 𝑈) → 𝐵 ∈ 𝑉) |
44 | 43 | ex 449 |
. . . . . . . . . . . . . . 15
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word (Vtx‘𝐺) ∧
(#‘〈“𝐴𝐵𝐶”〉) = (2 + 1)) → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉)) |
45 | 26, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (2 WWalkSN 𝐺) → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((〈“𝐴𝐵𝐶”〉 ∈ (2 WWalkSN 𝐺) ∧ ((〈“𝐴𝐵𝐶”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝐶”〉‘2) = 𝐶)) → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉)) |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((〈“𝐴𝐵𝐶”〉 ∈ (2 WWalkSN 𝐺) ∧ ((〈“𝐴𝐵𝐶”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝐶”〉‘2) = 𝐶)) → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉))) |
48 | 25, 47 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐶)} → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉))) |
49 | 19, 48 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) → (𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉))) |
50 | 49 | impd 446 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ∧ 𝐵 ∈ 𝑈) → 𝐵 ∈ 𝑉)) |
51 | 50 | impcom 445 |
. . . . . . . 8
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ∧ 𝐵 ∈ 𝑈) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
52 | | simprr 792 |
. . . . . . . 8
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ∧ 𝐵 ∈ 𝑈) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
53 | 9, 51, 52 | 3jca 1235 |
. . . . . . 7
⊢
(((〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) ∧ 𝐵 ∈ 𝑈) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
54 | 53 | exp31 628 |
. . . . . 6
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) → (𝐵 ∈ 𝑈 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
55 | 8, 54 | mpid 43 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(𝑎 ∈ 𝑉, 𝑐 ∈ 𝑉 ↦ {𝑤 ∈ (2 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘2) = 𝑐)})𝐶) → (𝐵 ∈ 𝑈 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
56 | 6, 55 | syl6bi 242 |
. . . 4
⊢ (𝐺 ∈ V →
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝐵 ∈ 𝑈 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
57 | 56 | com23 84 |
. . 3
⊢ (𝐺 ∈ V → (𝐵 ∈ 𝑈 → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
58 | 57 | impd 446 |
. 2
⊢ (𝐺 ∈ V → ((𝐵 ∈ 𝑈 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
59 | | df-wwlksnon 41035 |
. . . . . . . . . 10
⊢
WWalksNOn = (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ (𝑎 ∈
(Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})) |
60 | 59 | reldmmpt2 6669 |
. . . . . . . . 9
⊢ Rel dom
WWalksNOn |
61 | 60 | ovprc2 6583 |
. . . . . . . 8
⊢ (¬
𝐺 ∈ V → (2
WWalksNOn 𝐺) =
∅) |
62 | 61 | oveqd 6566 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V → (𝐴(2 WWalksNOn 𝐺)𝐶) = (𝐴∅𝐶)) |
63 | | 0ov 6580 |
. . . . . . 7
⊢ (𝐴∅𝐶) = ∅ |
64 | 62, 63 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝐺 ∈ V → (𝐴(2 WWalksNOn 𝐺)𝐶) = ∅) |
65 | 64 | eleq2d 2673 |
. . . . 5
⊢ (¬
𝐺 ∈ V →
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴𝐵𝐶”〉 ∈
∅)) |
66 | | noel 3878 |
. . . . . 6
⊢ ¬
〈“𝐴𝐵𝐶”〉 ∈
∅ |
67 | 66 | pm2.21i 115 |
. . . . 5
⊢
(〈“𝐴𝐵𝐶”〉 ∈ ∅ → (𝐵 ∈ 𝑈 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
68 | 65, 67 | syl6bi 242 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝐵 ∈ 𝑈 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
69 | 68 | com23 84 |
. . 3
⊢ (¬
𝐺 ∈ V → (𝐵 ∈ 𝑈 → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
70 | 69 | impd 446 |
. 2
⊢ (¬
𝐺 ∈ V → ((𝐵 ∈ 𝑈 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
71 | 58, 70 | pm2.61i 175 |
1
⊢ ((𝐵 ∈ 𝑈 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |