Proof of Theorem 1to2vfriswmgra
Step | Hyp | Ref
| Expression |
1 | | 1vwmgra 26530 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) |
2 | 1 | a1d 25 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
3 | 2 | expcom 450 |
. . 3
⊢ (𝑉 = {𝐴} → (𝐴 ∈ 𝑋 → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
4 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑉 = {𝐴, 𝐵} → (𝑉 FriendGrph 𝐸 ↔ {𝐴, 𝐵} FriendGrph 𝐸)) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → (𝑉 FriendGrph 𝐸 ↔ {𝐴, 𝐵} FriendGrph 𝐸)) |
6 | | pm3.22 464 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ (𝐵 ∈ V ∧ 𝐴 ≠ 𝐵))) |
7 | | anass 679 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V) ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ∈ 𝑋 ∧ (𝐵 ∈ V ∧ 𝐴 ≠ 𝐵))) |
8 | 6, 7 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V) ∧ 𝐴 ≠ 𝐵)) |
9 | | frgra2v 26526 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V) ∧ 𝐴 ≠ 𝐵) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |
11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) |
12 | 11 | pm2.21d 117 |
. . . . . . . 8
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → ({𝐴, 𝐵} FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
13 | 5, 12 | sylbid 229 |
. . . . . . 7
⊢ ((𝑉 = {𝐴, 𝐵} ∧ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋)) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
14 | 13 | expcom 450 |
. . . . . 6
⊢ (((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 ∈ 𝑋) → (𝑉 = {𝐴, 𝐵} → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
15 | 14 | ex 449 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ 𝑋 → (𝑉 = {𝐴, 𝐵} → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))))) |
16 | 15 | com23 84 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))))) |
17 | | ianor 508 |
. . . . . . 7
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) ↔ (¬ 𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵)) |
18 | | prprc2 4244 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ V → {𝐴, 𝐵} = {𝐴}) |
19 | | nne 2786 |
. . . . . . . . 9
⊢ (¬
𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) |
20 | | preq2 4213 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐴 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
21 | 20 | eqcoms 2618 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴, 𝐴}) |
22 | | dfsn2 4138 |
. . . . . . . . . 10
⊢ {𝐴} = {𝐴, 𝐴} |
23 | 21, 22 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
24 | 19, 23 | sylbi 206 |
. . . . . . . 8
⊢ (¬
𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐴}) |
25 | 18, 24 | jaoi 393 |
. . . . . . 7
⊢ ((¬
𝐵 ∈ V ∨ ¬ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} = {𝐴}) |
26 | 17, 25 | sylbi 206 |
. . . . . 6
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} = {𝐴}) |
27 | 26 | eqeq2d 2620 |
. . . . 5
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} ↔ 𝑉 = {𝐴})) |
28 | 27, 3 | syl6bi 242 |
. . . 4
⊢ (¬
(𝐵 ∈ V ∧ 𝐴 ≠ 𝐵) → (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))))) |
29 | 16, 28 | pm2.61i 175 |
. . 3
⊢ (𝑉 = {𝐴, 𝐵} → (𝐴 ∈ 𝑋 → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
30 | 3, 29 | jaoi 393 |
. 2
⊢ ((𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑋 → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
31 | 30 | impcom 445 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |