| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2pthon3v.e | . . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) | 
| 2 |  | edgval 29066 | . . . . . . . . . 10
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) | 
| 3 | 1, 2 | eqtri 2765 | . . . . . . . . 9
⊢ 𝐸 = ran (iEdg‘𝐺) | 
| 4 | 3 | eleq2i 2833 | . . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ 𝐸 ↔ {𝐴, 𝐵} ∈ ran (iEdg‘𝐺)) | 
| 5 |  | 2pthon3v.v | . . . . . . . . . . 11
⊢ 𝑉 = (Vtx‘𝐺) | 
| 6 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 7 | 5, 6 | uhgrf 29079 | . . . . . . . . . 10
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅})) | 
| 8 | 7 | ffnd 6737 | . . . . . . . . 9
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) | 
| 9 |  | fvelrnb 6969 | . . . . . . . . 9
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
({𝐴, 𝐵} ∈ ran (iEdg‘𝐺) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵})) | 
| 10 | 8, 9 | syl 17 | . . . . . . . 8
⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ ran (iEdg‘𝐺) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵})) | 
| 11 | 4, 10 | bitrid 283 | . . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝐴, 𝐵} ∈ 𝐸 ↔ ∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵})) | 
| 12 | 3 | eleq2i 2833 | . . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ 𝐸 ↔ {𝐵, 𝐶} ∈ ran (iEdg‘𝐺)) | 
| 13 |  | fvelrnb 6969 | . . . . . . . . 9
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
({𝐵, 𝐶} ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) | 
| 14 | 8, 13 | syl 17 | . . . . . . . 8
⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) | 
| 15 | 12, 14 | bitrid 283 | . . . . . . 7
⊢ (𝐺 ∈ UHGraph → ({𝐵, 𝐶} ∈ 𝐸 ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) | 
| 16 | 11, 15 | anbi12d 632 | . . . . . 6
⊢ (𝐺 ∈ UHGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}))) | 
| 17 | 16 | adantr 480 | . . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}))) | 
| 18 | 17 | adantr 480 | . . . 4
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}))) | 
| 19 |  | reeanv 3229 | . . . 4
⊢
(∃𝑖 ∈ dom
(iEdg‘𝐺)∃𝑗 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) ↔ (∃𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) | 
| 20 | 18, 19 | bitr4di 289 | . . 3
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ ∃𝑖 ∈ dom (iEdg‘𝐺)∃𝑗 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}))) | 
| 21 |  | df-s2 14887 | . . . . . . . 8
⊢
〈“𝑖𝑗”〉 =
(〈“𝑖”〉 ++ 〈“𝑗”〉) | 
| 22 | 21 | ovexi 7465 | . . . . . . 7
⊢
〈“𝑖𝑗”〉 ∈
V | 
| 23 |  | df-s3 14888 | . . . . . . . 8
⊢
〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | 
| 24 | 23 | ovexi 7465 | . . . . . . 7
⊢
〈“𝐴𝐵𝐶”〉 ∈ V | 
| 25 | 22, 24 | pm3.2i 470 | . . . . . 6
⊢
(〈“𝑖𝑗”〉 ∈ V ∧
〈“𝐴𝐵𝐶”〉 ∈ V) | 
| 26 |  | eqid 2737 | . . . . . . . 8
⊢
〈“𝐴𝐵𝐶”〉 = 〈“𝐴𝐵𝐶”〉 | 
| 27 |  | eqid 2737 | . . . . . . . 8
⊢
〈“𝑖𝑗”〉 =
〈“𝑖𝑗”〉 | 
| 28 |  | simp-4r 784 | . . . . . . . 8
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) | 
| 29 |  | 3simpb 1150 | . . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) | 
| 30 | 29 | ad3antlr 731 | . . . . . . . 8
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) | 
| 31 |  | eqimss2 4043 | . . . . . . . . . 10
⊢
(((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} → {𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖)) | 
| 32 |  | eqimss2 4043 | . . . . . . . . . 10
⊢
(((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶} → {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗)) | 
| 33 | 31, 32 | anim12i 613 | . . . . . . . . 9
⊢
((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖) ∧ {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))) | 
| 34 | 33 | adantl 481 | . . . . . . . 8
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ⊆ ((iEdg‘𝐺)‘𝑖) ∧ {𝐵, 𝐶} ⊆ ((iEdg‘𝐺)‘𝑗))) | 
| 35 |  | fveqeq2 6915 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ↔ ((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵})) | 
| 36 | 35 | anbi1d 631 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) ↔ (((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}))) | 
| 37 |  | eqtr2 2761 | . . . . . . . . . . . . . 14
⊢
((((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → {𝐴, 𝐵} = {𝐵, 𝐶}) | 
| 38 |  | 3simpa 1149 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) | 
| 39 |  | 3simpc 1151 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) | 
| 40 |  | preq12bg 4853 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) | 
| 41 | 38, 39, 40 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) | 
| 42 |  | eqneqall 2951 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝑖 ≠ 𝑗)) | 
| 43 | 42 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 𝑖 ≠ 𝑗)) | 
| 44 | 43 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 → 𝑖 ≠ 𝑗)) | 
| 45 | 44 | com12 32 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗)) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗)) | 
| 47 |  | eqneqall 2951 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐶 → (𝐴 ≠ 𝐶 → 𝑖 ≠ 𝑗)) | 
| 48 | 47 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ≠ 𝐶 → (𝐴 = 𝐶 → 𝑖 ≠ 𝑗)) | 
| 49 | 48 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐶 → 𝑖 ≠ 𝑗)) | 
| 50 | 49 | com12 32 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗)) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐵) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗)) | 
| 52 | 46, 51 | jaoi 858 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗)) | 
| 53 | 41, 52 | biimtrdi 253 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({𝐴, 𝐵} = {𝐵, 𝐶} → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝑖 ≠ 𝑗))) | 
| 54 | 53 | com23 86 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 𝑖 ≠ 𝑗))) | 
| 55 | 54 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 𝑖 ≠ 𝑗))) | 
| 56 | 55 | imp 406 | . . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 𝑖 ≠ 𝑗)) | 
| 57 | 56 | com12 32 | . . . . . . . . . . . . . 14
⊢ ({𝐴, 𝐵} = {𝐵, 𝐶} → (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → 𝑖 ≠ 𝑗)) | 
| 58 | 37, 57 | syl 17 | . . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘𝑗) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → 𝑖 ≠ 𝑗)) | 
| 59 | 36, 58 | biimtrdi 253 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → 𝑖 ≠ 𝑗))) | 
| 60 | 59 | com23 86 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → 𝑖 ≠ 𝑗))) | 
| 61 |  | 2a1 28 | . . . . . . . . . . 11
⊢ (𝑖 ≠ 𝑗 → (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → 𝑖 ≠ 𝑗))) | 
| 62 | 60, 61 | pm2.61ine 3025 | . . . . . . . . . 10
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → 𝑖 ≠ 𝑗)) | 
| 63 | 62 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → 𝑖 ≠ 𝑗)) | 
| 64 | 63 | imp 406 | . . . . . . . 8
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → 𝑖 ≠ 𝑗) | 
| 65 |  | simplr2 1217 | . . . . . . . . 9
⊢ ((((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) → 𝐴 ≠ 𝐶) | 
| 66 | 65 | adantr 480 | . . . . . . . 8
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → 𝐴 ≠ 𝐶) | 
| 67 | 26, 27, 28, 30, 34, 5, 6, 64, 66 | 2pthond 29962 | . . . . . . 7
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → 〈“𝑖𝑗”〉(𝐴(SPathsOn‘𝐺)𝐶)〈“𝐴𝐵𝐶”〉) | 
| 68 |  | s2len 14928 | . . . . . . 7
⊢
(♯‘〈“𝑖𝑗”〉) = 2 | 
| 69 | 67, 68 | jctir 520 | . . . . . 6
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → (〈“𝑖𝑗”〉(𝐴(SPathsOn‘𝐺)𝐶)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑖𝑗”〉) = 2)) | 
| 70 |  | breq12 5148 | . . . . . . . 8
⊢ ((𝑓 = 〈“𝑖𝑗”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → (𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ↔ 〈“𝑖𝑗”〉(𝐴(SPathsOn‘𝐺)𝐶)〈“𝐴𝐵𝐶”〉)) | 
| 71 |  | fveqeq2 6915 | . . . . . . . . 9
⊢ (𝑓 = 〈“𝑖𝑗”〉 → ((♯‘𝑓) = 2 ↔
(♯‘〈“𝑖𝑗”〉) = 2)) | 
| 72 | 71 | adantr 480 | . . . . . . . 8
⊢ ((𝑓 = 〈“𝑖𝑗”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → ((♯‘𝑓) = 2 ↔
(♯‘〈“𝑖𝑗”〉) = 2)) | 
| 73 | 70, 72 | anbi12d 632 | . . . . . . 7
⊢ ((𝑓 = 〈“𝑖𝑗”〉 ∧ 𝑝 = 〈“𝐴𝐵𝐶”〉) → ((𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2) ↔ (〈“𝑖𝑗”〉(𝐴(SPathsOn‘𝐺)𝐶)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑖𝑗”〉) = 2))) | 
| 74 | 73 | spc2egv 3599 | . . . . . 6
⊢
((〈“𝑖𝑗”〉 ∈ V ∧
〈“𝐴𝐵𝐶”〉 ∈ V) →
((〈“𝑖𝑗”〉(𝐴(SPathsOn‘𝐺)𝐶)〈“𝐴𝐵𝐶”〉 ∧
(♯‘〈“𝑖𝑗”〉) = 2) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2))) | 
| 75 | 25, 69, 74 | mpsyl 68 | . . . . 5
⊢
(((((𝐺 ∈
UHGraph ∧ (𝐴 ∈
𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) ∧ (((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶})) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2)) | 
| 76 | 75 | ex 412 | . . . 4
⊢ ((((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ∈ dom (iEdg‘𝐺) ∧ 𝑗 ∈ dom (iEdg‘𝐺))) → ((((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2))) | 
| 77 | 76 | rexlimdvva 3213 | . . 3
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (∃𝑖 ∈ dom (iEdg‘𝐺)∃𝑗 ∈ dom (iEdg‘𝐺)(((iEdg‘𝐺)‘𝑖) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘𝑗) = {𝐵, 𝐶}) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2))) | 
| 78 | 20, 77 | sylbid 240 | . 2
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2))) | 
| 79 | 78 | 3impia 1118 | 1
⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2)) |