Step | Hyp | Ref
| Expression |
1 | | neirr 2791 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝐴 ≠ 𝐴 |
2 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 ≠ 𝐴) |
3 | 2 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐴 ≠ 𝐴)) |
4 | 1, 3 | mtoi 189 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} USGrph 𝐸 → ¬ {𝐴, 𝐴} ∈ ran 𝐸) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ {𝐴, 𝐴} ∈ ran 𝐸) |
6 | 5 | intnanrd 954 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
7 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐴, 𝐴} ∈ V |
8 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐴, 𝐵} ∈ V |
9 | 7, 8 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝐴, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸) |
10 | 6, 9 | sylnib 317 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸) |
11 | | neirr 2791 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝐵 ≠ 𝐵 |
12 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵} USGrph 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) → 𝐵 ≠ 𝐵) |
13 | 12 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} USGrph 𝐸 → ({𝐵, 𝐵} ∈ ran 𝐸 → 𝐵 ≠ 𝐵)) |
14 | 11, 13 | mtoi 189 |
. . . . . . . . . . . . . . 15
⊢ ({𝐴, 𝐵} USGrph 𝐸 → ¬ {𝐵, 𝐵} ∈ ran 𝐸) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ {𝐵, 𝐵} ∈ ran 𝐸) |
16 | 15 | intnand 953 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸)) |
17 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐵, 𝐴} ∈ V |
18 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢ {𝐵, 𝐵} ∈ V |
19 | 17, 18 | prss 4291 |
. . . . . . . . . . . . 13
⊢ (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐵} ∈ ran 𝐸) ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸) |
20 | 16, 19 | sylnib 317 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸) |
21 | | ioran 510 |
. . . . . . . . . . . 12
⊢ (¬
({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸) ↔ (¬ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∧ ¬ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸)) |
22 | 10, 20, 21 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸)) |
23 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → {𝑥, 𝐴} = {𝐴, 𝐴}) |
24 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵}) |
25 | 23, 24 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐴, 𝐴}, {𝐴, 𝐵}}) |
26 | 25 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸)) |
27 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐵 → {𝑥, 𝐴} = {𝐵, 𝐴}) |
28 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐵 → {𝑥, 𝐵} = {𝐵, 𝐵}) |
29 | 27, 28 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝐵}} = {{𝐵, 𝐴}, {𝐵, 𝐵}}) |
30 | 29 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸)) |
31 | 26, 30 | rexprg 4182 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸))) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({{𝐴, 𝐴}, {𝐴, 𝐵}} ⊆ ran 𝐸 ∨ {{𝐵, 𝐴}, {𝐵, 𝐵}} ⊆ ran 𝐸))) |
33 | 22, 32 | mtbird 314 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ∃𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) |
34 | | reurex 3137 |
. . . . . . . . . 10
⊢
(∃!𝑥 ∈
{𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 → ∃𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) |
35 | 33, 34 | nsyl 134 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) |
36 | 35 | orcd 406 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∨ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
37 | | rexnal 2978 |
. . . . . . . . . . . 12
⊢
(∃𝑙 ∈
({𝐴, 𝐵} ∖ {𝐴}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
38 | 37 | bicomi 213 |
. . . . . . . . . . 11
⊢ (¬
∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
40 | | difprsn1 4271 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) |
41 | 40 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵}) |
42 | 41 | rexeqdv 3122 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ {𝐵} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
43 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝐵 → {𝑥, 𝑙} = {𝑥, 𝐵}) |
44 | 43 | preq2d 4219 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝐵 → {{𝑥, 𝐴}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝐵}}) |
45 | 44 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝐵 → ({{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
46 | 45 | reubidv 3103 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
47 | 46 | notbid 307 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝐵 → (¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
48 | 47 | rexsng 4166 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑌 → (∃𝑙 ∈ {𝐵} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
49 | 48 | ad3antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑙 ∈ {𝐵} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
50 | 39, 42, 49 | 3bitrd 293 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸)) |
51 | | rexnal 2978 |
. . . . . . . . . . . 12
⊢
(∃𝑙 ∈
({𝐴, 𝐵} ∖ {𝐵}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
52 | 51 | bicomi 213 |
. . . . . . . . . . 11
⊢ (¬
∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
53 | 52 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
54 | | difprsn2 4272 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) |
55 | 54 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴}) |
56 | 55 | rexeqdv 3122 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵}) ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃𝑙 ∈ {𝐴} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
57 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝐴 → {𝑥, 𝑙} = {𝑥, 𝐴}) |
58 | 57 | preq2d 4219 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝐴 → {{𝑥, 𝐵}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝐴}}) |
59 | 58 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝐴 → ({{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
60 | 59 | reubidv 3103 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
61 | 60 | notbid 307 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝐴 → (¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
62 | 61 | rexsng 4166 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑋 → (∃𝑙 ∈ {𝐴} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
63 | 62 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑙 ∈ {𝐴} ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
64 | 53, 56, 63 | 3bitrd 293 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸)) |
65 | 50, 64 | orbi12d 742 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ((¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∨ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸) ↔ (¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ∨ ¬ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝐴}} ⊆ ran 𝐸))) |
66 | 36, 65 | mpbird 246 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∨ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
67 | | sneq 4135 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → {𝑘} = {𝐴}) |
68 | 67 | difeq2d 3690 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ({𝐴, 𝐵} ∖ {𝑘}) = ({𝐴, 𝐵} ∖ {𝐴})) |
69 | | preq2 4213 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐴 → {𝑥, 𝑘} = {𝑥, 𝐴}) |
70 | 69 | preq1d 4218 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐴 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐴}, {𝑥, 𝑙}}) |
71 | 70 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
72 | 71 | reubidv 3103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
73 | 68, 72 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
74 | 73 | notbid 307 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
75 | | sneq 4135 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐵 → {𝑘} = {𝐵}) |
76 | 75 | difeq2d 3690 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐵 → ({𝐴, 𝐵} ∖ {𝑘}) = ({𝐴, 𝐵} ∖ {𝐵})) |
77 | | preq2 4213 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐵 → {𝑥, 𝑘} = {𝑥, 𝐵}) |
78 | 77 | preq1d 4218 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐵 → {{𝑥, 𝑘}, {𝑥, 𝑙}} = {{𝑥, 𝐵}, {𝑥, 𝑙}}) |
79 | 78 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐵 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
80 | 79 | reubidv 3103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐵 → (∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
81 | 76, 80 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐵 → (∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
82 | 81 | notbid 307 |
. . . . . . . . 9
⊢ (𝑘 = 𝐵 → (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
83 | 74, 82 | rexprg 4182 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑘 ∈ {𝐴, 𝐵} ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∨ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |
84 | 83 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → (∃𝑘 ∈ {𝐴, 𝐵} ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ (¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐴})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐴}, {𝑥, 𝑙}} ⊆ ran 𝐸 ∨ ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝐵})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝐵}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |
85 | 66, 84 | mpbird 246 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ∃𝑘 ∈ {𝐴, 𝐵} ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
86 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑘 ∈
{𝐴, 𝐵} ¬ ∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸 ↔ ¬ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
87 | 85, 86 | sylib 207 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸) |
88 | 87 | intnand 953 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
89 | | usgrav 25867 |
. . . . . 6
⊢ ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V)) |
90 | 89 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V)) |
91 | | isfrgra 26517 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V) → ({𝐴, 𝐵} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ({𝐴, 𝐵} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑙 ∈ ({𝐴, 𝐵} ∖ {𝑘})∃!𝑥 ∈ {𝐴, 𝐵} {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |
93 | 88, 92 | mtbird 314 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) ∧ {𝐴, 𝐵} USGrph 𝐸) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |
94 | 93 | expcom 450 |
. 2
⊢ ({𝐴, 𝐵} USGrph 𝐸 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ¬ {𝐴, 𝐵} FriendGrph 𝐸)) |
95 | | frisusgra 26519 |
. . . 4
⊢ ({𝐴, 𝐵} FriendGrph 𝐸 → {𝐴, 𝐵} USGrph 𝐸) |
96 | 95 | con3i 149 |
. . 3
⊢ (¬
{𝐴, 𝐵} USGrph 𝐸 → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |
97 | 96 | a1d 25 |
. 2
⊢ (¬
{𝐴, 𝐵} USGrph 𝐸 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ¬ {𝐴, 𝐵} FriendGrph 𝐸)) |
98 | 94, 97 | pm2.61i 175 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |