| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 3 | 1, 2 | grilcbri 47969 |
. . 3
⊢ (𝐺
≃𝑙𝑔𝑟 𝑆 → ∃𝑓(𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))))) |
| 4 | | grlicrcl 47967 |
. . 3
⊢ (𝐺
≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V)) |
| 5 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
| 6 | | cnvexg 7946 |
. . . . . . . . . 10
⊢ (𝑓 ∈ V → ◡𝑓 ∈ V) |
| 7 | 5, 6 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ◡𝑓 ∈ V) |
| 8 | | f1ocnv 6860 |
. . . . . . . . . . 11
⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → ◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺)) |
| 9 | 8 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺)) |
| 10 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆)) → (◡𝑓‘𝑤) ∈ (Vtx‘𝐺)) |
| 11 | 10 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (◡𝑓‘𝑤) ∈ (Vtx‘𝐺)) |
| 12 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (◡𝑓‘𝑤) → (𝐺 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (◡𝑓‘𝑤) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) = (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤)))) |
| 14 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (◡𝑓‘𝑤) → (𝑓‘𝑣) = (𝑓‘(◡𝑓‘𝑤))) |
| 15 | 14 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (◡𝑓‘𝑤) → (𝑆 ClNeighbVtx (𝑓‘𝑣)) = (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))) |
| 16 | 15 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (◡𝑓‘𝑤) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤))))) |
| 17 | 13, 16 | breq12d 5156 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (◡𝑓‘𝑤) → ((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))))) |
| 18 | 17 | rspcv 3618 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓‘𝑤) ∈ (Vtx‘𝐺) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))))) |
| 19 | 11, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))))) |
| 20 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆)) → (𝑓‘(◡𝑓‘𝑤)) = 𝑤) |
| 21 | 20 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑓‘(◡𝑓‘𝑤)) = 𝑤) |
| 22 | 21 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤))) = (𝑆 ClNeighbVtx 𝑤)) |
| 23 | 22 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))) = (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤))) |
| 24 | 23 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)))) |
| 25 | | simp3 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → 𝐺 ∈ UHGraph) |
| 26 | 1 | clnbgrssvtx 47818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ClNeighbVtx (◡𝑓‘𝑤)) ⊆ (Vtx‘𝐺) |
| 27 | 1 | isubgruhgr 47854 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ UHGraph ∧ (𝐺 ClNeighbVtx (◡𝑓‘𝑤)) ⊆ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ∈ UHGraph) |
| 28 | 25, 26, 27 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ∈ UHGraph) |
| 29 | | gricsym 47890 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ∈ UHGraph → ((𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 31 | 24, 30 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → ((𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘(◡𝑓‘𝑤)))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 32 | 19, 31 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ 𝑤 ∈ (Vtx‘𝑆) ∧ 𝐺 ∈ UHGraph) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 33 | 32 | 3exp 1120 |
. . . . . . . . . . . . 13
⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → (𝑤 ∈ (Vtx‘𝑆) → (𝐺 ∈ UHGraph → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))))) |
| 34 | 33 | com24 95 |
. . . . . . . . . . . 12
⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣))) → (𝐺 ∈ UHGraph → (𝑤 ∈ (Vtx‘𝑆) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))))) |
| 35 | 34 | imp31 417 |
. . . . . . . . . . 11
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → (𝑤 ∈ (Vtx‘𝑆) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 36 | 35 | ralrimiv 3145 |
. . . . . . . . . 10
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤)))) |
| 37 | 9, 36 | jca 511 |
. . . . . . . . 9
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → (◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 38 | | f1oeq1 6836 |
. . . . . . . . . 10
⊢ (𝑔 = ◡𝑓 → (𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ↔ ◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺))) |
| 39 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = ◡𝑓 → (𝑔‘𝑤) = (◡𝑓‘𝑤)) |
| 40 | 39 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑔 = ◡𝑓 → (𝐺 ClNeighbVtx (𝑔‘𝑤)) = (𝐺 ClNeighbVtx (◡𝑓‘𝑤))) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑔 = ◡𝑓 → (𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) = (𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤)))) |
| 42 | 41 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑔 = ◡𝑓 → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 43 | 42 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑔 = ◡𝑓 → (∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))) ↔ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤))))) |
| 44 | 38, 43 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑔 = ◡𝑓 → ((𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))) ↔ (◡𝑓:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (◡𝑓‘𝑤)))))) |
| 45 | 7, 37, 44 | spcedv 3598 |
. . . . . . . 8
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph) → ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))))) |
| 46 | 45 | 3adant3 1133 |
. . . . . . 7
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤))))) |
| 47 | 2, 1 | dfgrlic2 47968 |
. . . . . . . . 9
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆
≃𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))))) |
| 48 | 47 | ancoms 458 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝑆
≃𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))))) |
| 49 | 48 | 3ad2ant3 1136 |
. . . . . . 7
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → (𝑆
≃𝑙𝑔𝑟 𝐺 ↔ ∃𝑔(𝑔:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝐺) ∧ ∀𝑤 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑤)) ≃𝑔𝑟
(𝐺 ISubGr (𝐺 ClNeighbVtx (𝑔‘𝑤)))))) |
| 50 | 46, 49 | mpbird 257 |
. . . . . 6
⊢ (((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) ∧ 𝐺 ∈ UHGraph ∧ (𝐺 ∈ V ∧ 𝑆 ∈ V)) → 𝑆
≃𝑙𝑔𝑟 𝐺) |
| 51 | 50 | 3exp 1120 |
. . . . 5
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → (𝐺 ∈ UHGraph → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → 𝑆
≃𝑙𝑔𝑟 𝐺))) |
| 52 | 51 | com23 86 |
. . . 4
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝐺 ∈ UHGraph → 𝑆
≃𝑙𝑔𝑟 𝐺))) |
| 53 | 52 | exlimiv 1930 |
. . 3
⊢
(∃𝑓(𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝑆 ISubGr (𝑆 ClNeighbVtx (𝑓‘𝑣)))) → ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝐺 ∈ UHGraph → 𝑆
≃𝑙𝑔𝑟 𝐺))) |
| 54 | 3, 4, 53 | sylc 65 |
. 2
⊢ (𝐺
≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ UHGraph → 𝑆
≃𝑙𝑔𝑟 𝐺)) |
| 55 | 54 | com12 32 |
1
⊢ (𝐺 ∈ UHGraph → (𝐺
≃𝑙𝑔𝑟 𝑆 → 𝑆
≃𝑙𝑔𝑟 𝐺)) |