Proof of Theorem frgranbnb
Step | Hyp | Ref
| Expression |
1 | | frgranbnb.f |
. . . 4
⊢ (𝜑 → 𝑉 FriendGrph 𝐸) |
2 | | frisusgra 26519 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑉 USGrph 𝐸) |
4 | | frgranbnb.nx |
. . . . . . . . . 10
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) |
5 | 4 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑈 ∈ 𝐷 ↔ 𝑈 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
6 | | nbgraeledg 25959 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ {𝑈, 𝑋} ∈ ran 𝐸)) |
7 | 6 | biimpd 218 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → {𝑈, 𝑋} ∈ ran 𝐸)) |
8 | 5, 7 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ 𝐷 → {𝑈, 𝑋} ∈ ran 𝐸)) |
9 | 4 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑊 ∈ 𝐷 ↔ 𝑊 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
10 | | nbgraeledg 25959 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) ↔ {𝑊, 𝑋} ∈ ran 𝐸)) |
11 | 10 | biimpd 218 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → {𝑊, 𝑋} ∈ ran 𝐸)) |
12 | 9, 11 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ 𝐷 → {𝑊, 𝑋} ∈ ran 𝐸)) |
13 | 8, 12 | anim12d 584 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ((𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) → ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸))) |
14 | 13 | imp 444 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷)) → ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) |
15 | | nbgraisvtx 25960 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → 𝑈 ∈ 𝑉)) |
16 | 5, 15 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑈 ∈ 𝐷 → 𝑈 ∈ 𝑉)) |
17 | | nbgraisvtx 25960 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → 𝑊 ∈ 𝑉)) |
18 | 9, 17 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ 𝐷 → 𝑊 ∈ 𝑉)) |
19 | 16, 18 | anim12d 584 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → ((𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) → (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) |
20 | 19 | imp 444 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷)) → (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) |
21 | | usgraedgrnv 25906 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑈, 𝐴} ∈ ran 𝐸) → (𝑈 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
22 | 21 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝑈 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
23 | | frgranbnb.x |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
24 | | ax-1 6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = 𝑋 → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)) |
25 | 24 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 = 𝑋 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)))) |
26 | 25 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = 𝑋 → (𝑈 ≠ 𝑊 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)))))) |
27 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → 𝑉 USGrph 𝐸) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑉 USGrph 𝐸) |
29 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → 𝑊 ∈ 𝑉) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑊 ∈ 𝑉) |
31 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝑈 ∈ 𝑉) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → 𝑈 ∈ 𝑉) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → 𝑈 ∈ 𝑉) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑈 ∈ 𝑉) |
35 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑈 ≠ 𝑊 ↔ 𝑊 ≠ 𝑈) |
36 | 35 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑈 ≠ 𝑊 → 𝑊 ≠ 𝑈) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝑊 ≠ 𝑈) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑊 ≠ 𝑈) |
39 | 30, 34, 38 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈)) |
40 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → 𝑋 ∈ 𝑉) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → 𝑋 ∈ 𝑉) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑋 ∈ 𝑉) |
44 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → 𝐴 ∈ 𝑉) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝐴 ∈ 𝑉) |
46 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐴 ≠ 𝑋 ↔ 𝑋 ≠ 𝐴) |
47 | 46 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐴 ≠ 𝑋 → 𝑋 ≠ 𝐴) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝑋 ≠ 𝐴) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → 𝑋 ≠ 𝐴) |
50 | 43, 45, 49 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴)) |
51 | 28, 39, 50 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴))) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → (𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴)))) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → (𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴)))) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → (𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴)))) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴))) |
56 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ {𝑈, 𝑋} = {𝑋, 𝑈} |
57 | 56 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ({𝑈, 𝑋} ∈ ran 𝐸 ↔ {𝑋, 𝑈} ∈ ran 𝐸) |
58 | 57 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ({𝑈, 𝑋} ∈ ran 𝐸 → {𝑋, 𝑈} ∈ ran 𝐸) |
59 | 58 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → ({𝑋, 𝑈} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) |
60 | 59 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → ({𝑊, 𝑋} ∈ ran 𝐸 ∧ {𝑋, 𝑈} ∈ ran 𝐸)) |
61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ({𝑊, 𝑋} ∈ ran 𝐸 ∧ {𝑋, 𝑈} ∈ ran 𝐸)) |
62 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ {𝑊, 𝐴} = {𝐴, 𝑊} |
63 | 62 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ({𝑊, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝑊} ∈ ran 𝐸) |
64 | 63 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ({𝑊, 𝐴} ∈ ran 𝐸 → {𝐴, 𝑊} ∈ ran 𝐸) |
65 | 64 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝑊} ∈ ran 𝐸)) |
66 | 61, 65 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (({𝑊, 𝑋} ∈ ran 𝐸 ∧ {𝑋, 𝑈} ∈ ran 𝐸) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝑊} ∈ ran 𝐸))) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (({𝑊, 𝑋} ∈ ran 𝐸 ∧ {𝑋, 𝑈} ∈ ran 𝐸) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝑊} ∈ ran 𝐸))) |
68 | | 4cyclusnfrgra 26546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑊 ∈ 𝑉 ∧ 𝑈 ∈ 𝑉 ∧ 𝑊 ≠ 𝑈) ∧ (𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ≠ 𝐴)) → ((({𝑊, 𝑋} ∈ ran 𝐸 ∧ {𝑋, 𝑈} ∈ ran 𝐸) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝑊} ∈ ran 𝐸)) → ¬ 𝑉 FriendGrph 𝐸)) |
69 | 55, 67, 68 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → ¬ 𝑉 FriendGrph 𝐸) |
70 | 69 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) ∧ (𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)) |
71 | 70 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋))) |
72 | 71 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑉 USGrph 𝐸 ∧ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉))) ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝑉 FriendGrph 𝐸 → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝐴 = 𝑋))) |
73 | 72 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑉 USGrph 𝐸 → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (𝑉 FriendGrph 𝐸 → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝐴 = 𝑋)))))) |
74 | 73 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑉 USGrph 𝐸 → (𝑉 FriendGrph 𝐸 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝐴 = 𝑋)))))) |
75 | 2, 74 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑉 FriendGrph 𝐸 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → 𝐴 = 𝑋))))) |
76 | 75 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝑋 ∧ 𝑈 ≠ 𝑊) → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋))))) |
77 | 76 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ≠ 𝑋 → (𝑈 ≠ 𝑊 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)))))) |
78 | 26, 77 | pm2.61ine 2865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑈 ≠ 𝑊 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋))))) |
79 | 78 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)))) |
80 | 79 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉)) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋)))) |
81 | 80 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → (𝑉 FriendGrph 𝐸 → 𝐴 = 𝑋))))) |
82 | 81 | com25 97 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑉 FriendGrph 𝐸 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
83 | 82 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋)))))) |
84 | 83 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → (𝐴 ∈ 𝑉 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋)))))) |
85 | 23, 1, 84 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ 𝑉 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
86 | 85 | com13 86 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (𝐴 ∈ 𝑉 → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
88 | 87 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ((𝑉 USGrph 𝐸 ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → ((𝑉 USGrph 𝐸 ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
90 | 22, 89 | mpcom 37 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸)) → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋)))) |
91 | 90 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → 𝐴 = 𝑋))))) |
92 | 91 | com25 97 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (𝜑 → ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋))))) |
93 | 92 | com14 94 |
. . . . . . . . 9
⊢ ((𝑈 ≠ 𝑊 ∧ ({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸)) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (𝜑 → (𝑉 USGrph 𝐸 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋))))) |
94 | 93 | ex 449 |
. . . . . . . 8
⊢ (𝑈 ≠ 𝑊 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (𝜑 → (𝑉 USGrph 𝐸 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)))))) |
95 | 94 | com15 99 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (𝜑 → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)))))) |
96 | 95 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷)) → (({𝑈, 𝑋} ∈ ran 𝐸 ∧ {𝑊, 𝑋} ∈ ran 𝐸) → ((𝑈 ∈ 𝑉 ∧ 𝑊 ∈ 𝑉) → (𝜑 → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)))))) |
97 | 14, 20, 96 | mp2d 47 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷)) → (𝜑 → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)))) |
98 | 97 | ex 449 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → ((𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) → (𝜑 → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋))))) |
99 | 98 | com23 84 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝜑 → ((𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋))))) |
100 | 3, 99 | mpcom 37 |
. 2
⊢ (𝜑 → ((𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) → (𝑈 ≠ 𝑊 → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)))) |
101 | 100 | 3imp 1249 |
1
⊢ ((𝜑 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) ∧ 𝑈 ≠ 𝑊) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)) |