Proof of Theorem usgraedgprv
Step | Hyp | Ref
| Expression |
1 | | usgrass 25890 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → (𝐸‘𝑋) ⊆ 𝑉) |
2 | | usgraedg2 25904 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → (#‘(𝐸‘𝑋)) = 2) |
3 | | sseq1 3589 |
. . . . 5
⊢ ((𝐸‘𝑋) = {𝑀, 𝑁} → ((𝐸‘𝑋) ⊆ 𝑉 ↔ {𝑀, 𝑁} ⊆ 𝑉)) |
4 | | fveq2 6103 |
. . . . . 6
⊢ ((𝐸‘𝑋) = {𝑀, 𝑁} → (#‘(𝐸‘𝑋)) = (#‘{𝑀, 𝑁})) |
5 | 4 | eqeq1d 2612 |
. . . . 5
⊢ ((𝐸‘𝑋) = {𝑀, 𝑁} → ((#‘(𝐸‘𝑋)) = 2 ↔ (#‘{𝑀, 𝑁}) = 2)) |
6 | 3, 5 | anbi12d 743 |
. . . 4
⊢ ((𝐸‘𝑋) = {𝑀, 𝑁} → (((𝐸‘𝑋) ⊆ 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) ↔ ({𝑀, 𝑁} ⊆ 𝑉 ∧ (#‘{𝑀, 𝑁}) = 2))) |
7 | | prssg 4290 |
. . . . . . 7
⊢ ((𝑀 ∈ V ∧ 𝑁 ∈ V) → ((𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ↔ {𝑀, 𝑁} ⊆ 𝑉)) |
8 | 7 | biimprd 237 |
. . . . . 6
⊢ ((𝑀 ∈ V ∧ 𝑁 ∈ V) → ({𝑀, 𝑁} ⊆ 𝑉 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
9 | 8 | adantrd 483 |
. . . . 5
⊢ ((𝑀 ∈ V ∧ 𝑁 ∈ V) → (({𝑀, 𝑁} ⊆ 𝑉 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
10 | | ianor 508 |
. . . . . 6
⊢ (¬
(𝑀 ∈ V ∧ 𝑁 ∈ V) ↔ (¬ 𝑀 ∈ V ∨ ¬ 𝑁 ∈ V)) |
11 | | prprc1 4243 |
. . . . . . . . . . 11
⊢ (¬
𝑀 ∈ V → {𝑀, 𝑁} = {𝑁}) |
12 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ({𝑀, 𝑁} = {𝑁} → (#‘{𝑀, 𝑁}) = (#‘{𝑁})) |
13 | | hashsng 13020 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → (#‘{𝑁}) = 1) |
14 | 12, 13 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ V ∧ {𝑀, 𝑁} = {𝑁}) → (#‘{𝑀, 𝑁}) = 1) |
15 | | eqtr2 2630 |
. . . . . . . . . . . . . . 15
⊢
(((#‘{𝑀, 𝑁}) = 1 ∧ (#‘{𝑀, 𝑁}) = 2) → 1 = 2) |
16 | | 1ne2 11117 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ≠
2 |
17 | 16 | neii 2784 |
. . . . . . . . . . . . . . . 16
⊢ ¬ 1
= 2 |
18 | 17 | pm2.21i 115 |
. . . . . . . . . . . . . . 15
⊢ (1 = 2
→ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
19 | 15, 18 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((#‘{𝑀, 𝑁}) = 1 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
20 | 19 | ex 449 |
. . . . . . . . . . . . 13
⊢
((#‘{𝑀, 𝑁}) = 1 → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
21 | 14, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ V ∧ {𝑀, 𝑁} = {𝑁}) → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
22 | 21 | expcom 450 |
. . . . . . . . . . 11
⊢ ({𝑀, 𝑁} = {𝑁} → (𝑁 ∈ V → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
23 | 11, 22 | syl 17 |
. . . . . . . . . 10
⊢ (¬
𝑀 ∈ V → (𝑁 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
24 | 23 | com12 32 |
. . . . . . . . 9
⊢ (𝑁 ∈ V → (¬ 𝑀 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
25 | | prprc 4245 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 ∈ V ∧ ¬
𝑀 ∈ V) → {𝑁, 𝑀} = ∅) |
26 | | prcom 4211 |
. . . . . . . . . . . . 13
⊢ {𝑁, 𝑀} = {𝑀, 𝑁} |
27 | 26 | eqeq1i 2615 |
. . . . . . . . . . . 12
⊢ ({𝑁, 𝑀} = ∅ ↔ {𝑀, 𝑁} = ∅) |
28 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ ({𝑀, 𝑁} = ∅ → (#‘{𝑀, 𝑁}) = (#‘∅)) |
29 | | hash0 13019 |
. . . . . . . . . . . . 13
⊢
(#‘∅) = 0 |
30 | 28, 29 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ({𝑀, 𝑁} = ∅ → (#‘{𝑀, 𝑁}) = 0) |
31 | 27, 30 | sylbi 206 |
. . . . . . . . . . 11
⊢ ({𝑁, 𝑀} = ∅ → (#‘{𝑀, 𝑁}) = 0) |
32 | | eqtr2 2630 |
. . . . . . . . . . . . 13
⊢
(((#‘{𝑀, 𝑁}) = 0 ∧ (#‘{𝑀, 𝑁}) = 2) → 0 = 2) |
33 | | 2ne0 10990 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
34 | 33 | nesymi 2839 |
. . . . . . . . . . . . . 14
⊢ ¬ 0
= 2 |
35 | 34 | pm2.21i 115 |
. . . . . . . . . . . . 13
⊢ (0 = 2
→ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
36 | 32, 35 | syl 17 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑀, 𝑁}) = 0 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
37 | 36 | ex 449 |
. . . . . . . . . . 11
⊢
((#‘{𝑀, 𝑁}) = 0 → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
38 | 25, 31, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((¬
𝑁 ∈ V ∧ ¬
𝑀 ∈ V) →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
39 | 38 | ex 449 |
. . . . . . . . 9
⊢ (¬
𝑁 ∈ V → (¬
𝑀 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
40 | 24, 39 | pm2.61i 175 |
. . . . . . . 8
⊢ (¬
𝑀 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
41 | | prprc2 4244 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ V → {𝑀, 𝑁} = {𝑀}) |
42 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ({𝑀, 𝑁} = {𝑀} → (#‘{𝑀, 𝑁}) = (#‘{𝑀})) |
43 | | hashsng 13020 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ V → (#‘{𝑀}) = 1) |
44 | 42, 43 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ V ∧ {𝑀, 𝑁} = {𝑀}) → (#‘{𝑀, 𝑁}) = 1) |
45 | 44, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ V ∧ {𝑀, 𝑁} = {𝑀}) → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
46 | 45 | expcom 450 |
. . . . . . . . . . 11
⊢ ({𝑀, 𝑁} = {𝑀} → (𝑀 ∈ V → ((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
47 | 41, 46 | syl 17 |
. . . . . . . . . 10
⊢ (¬
𝑁 ∈ V → (𝑀 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
48 | 47 | com12 32 |
. . . . . . . . 9
⊢ (𝑀 ∈ V → (¬ 𝑁 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
49 | | prprc 4245 |
. . . . . . . . . . 11
⊢ ((¬
𝑀 ∈ V ∧ ¬
𝑁 ∈ V) → {𝑀, 𝑁} = ∅) |
50 | 49, 30, 37 | 3syl 18 |
. . . . . . . . . 10
⊢ ((¬
𝑀 ∈ V ∧ ¬
𝑁 ∈ V) →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
51 | 50 | ex 449 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ V → (¬
𝑁 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)))) |
52 | 48, 51 | pm2.61i 175 |
. . . . . . . 8
⊢ (¬
𝑁 ∈ V →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
53 | 40, 52 | jaoi 393 |
. . . . . . 7
⊢ ((¬
𝑀 ∈ V ∨ ¬ 𝑁 ∈ V) →
((#‘{𝑀, 𝑁}) = 2 → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
54 | 53 | adantld 482 |
. . . . . 6
⊢ ((¬
𝑀 ∈ V ∨ ¬ 𝑁 ∈ V) → (({𝑀, 𝑁} ⊆ 𝑉 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
55 | 10, 54 | sylbi 206 |
. . . . 5
⊢ (¬
(𝑀 ∈ V ∧ 𝑁 ∈ V) → (({𝑀, 𝑁} ⊆ 𝑉 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
56 | 9, 55 | pm2.61i 175 |
. . . 4
⊢ (({𝑀, 𝑁} ⊆ 𝑉 ∧ (#‘{𝑀, 𝑁}) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
57 | 6, 56 | syl6bi 242 |
. . 3
⊢ ((𝐸‘𝑋) = {𝑀, 𝑁} → (((𝐸‘𝑋) ⊆ 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
58 | 57 | com12 32 |
. 2
⊢ (((𝐸‘𝑋) ⊆ 𝑉 ∧ (#‘(𝐸‘𝑋)) = 2) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |
59 | 1, 2, 58 | syl2anc 691 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) |