| Step | Hyp | Ref
| Expression |
| 1 | | df-grlim 47945 |
. . 3
⊢
GraphLocIso = (𝑔 ∈ V,
ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))}) |
| 2 | | elex 3501 |
. . . 4
⊢ (𝐺 ∈ 𝑋 → 𝐺 ∈ V) |
| 3 | 2 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → 𝐺 ∈ V) |
| 4 | | elex 3501 |
. . . 4
⊢ (𝐻 ∈ 𝑌 → 𝐻 ∈ V) |
| 5 | 4 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → 𝐻 ∈ V) |
| 6 | | f1of 6848 |
. . . . . 6
⊢ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) → 𝑓:(Vtx‘𝐺)⟶(Vtx‘𝐻)) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))) → 𝑓:(Vtx‘𝐺)⟶(Vtx‘𝐻)) |
| 8 | 7 | adantl 481 |
. . . 4
⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) ∧ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))) → 𝑓:(Vtx‘𝐺)⟶(Vtx‘𝐻)) |
| 9 | | fvexd 6921 |
. . . 4
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (Vtx‘𝐺) ∈ V) |
| 10 | | fvexd 6921 |
. . . 4
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (Vtx‘𝐻) ∈ V) |
| 11 | 8, 9, 10 | fabexd 7959 |
. . 3
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))} ∈ V) |
| 12 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → 𝑓 = 𝑓) |
| 13 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (Vtx‘𝑔) = (Vtx‘𝐺)) |
| 15 | | fveq2 6906 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (Vtx‘ℎ) = (Vtx‘𝐻)) |
| 16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (Vtx‘ℎ) = (Vtx‘𝐻)) |
| 17 | 12, 14, 16 | f1oeq123d 6842 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ↔ 𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻))) |
| 18 | | id 22 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → 𝑔 = 𝐺) |
| 19 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑔 ClNeighbVtx 𝑣) = (𝐺 ClNeighbVtx 𝑣)) |
| 20 | 18, 19 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) = (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣))) |
| 21 | | id 22 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → ℎ = 𝐻) |
| 22 | | oveq1 7438 |
. . . . . . . 8
⊢ (ℎ = 𝐻 → (ℎ ClNeighbVtx (𝑓‘𝑣)) = (𝐻 ClNeighbVtx (𝑓‘𝑣))) |
| 23 | 21, 22 | oveq12d 7449 |
. . . . . . 7
⊢ (ℎ = 𝐻 → (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))) = (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))) |
| 24 | 20, 23 | breqan12d 5159 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → ((𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))) |
| 25 | 14, 24 | raleqbidv 3346 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))) ↔ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))) |
| 26 | 17, 25 | anbi12d 632 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → ((𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣)))) ↔ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))) |
| 27 | 26 | abbidv 2808 |
. . 3
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))} = {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))}) |
| 28 | 1, 3, 5, 11, 27 | elovmpod 7677 |
. 2
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ 𝐹 ∈ {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))})) |
| 29 | | f1oeq1 6836 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ↔ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻))) |
| 30 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (𝑓‘𝑣) = (𝐹‘𝑣)) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝐻 ClNeighbVtx (𝑓‘𝑣)) = (𝐻 ClNeighbVtx (𝐹‘𝑣))) |
| 32 | 31 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))) = (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))) |
| 33 | 32 | breq2d 5155 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))) ↔ (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))))) |
| 34 | 33 | ralbidv 3178 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))) ↔ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))))) |
| 35 | 29, 34 | anbi12d 632 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))) ↔ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |
| 36 | 35 | elabg 3676 |
. . . 4
⊢ (𝐹 ∈ 𝑍 → (𝐹 ∈ {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))} ↔ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |
| 37 | 36 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))} ↔ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |
| 38 | | isgrlim.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 39 | | isgrlim.w |
. . . . 5
⊢ 𝑊 = (Vtx‘𝐻) |
| 40 | | f1oeq23 6839 |
. . . . 5
⊢ ((𝑉 = (Vtx‘𝐺) ∧ 𝑊 = (Vtx‘𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ↔ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻))) |
| 41 | 38, 39, 40 | mp2an 692 |
. . . 4
⊢ (𝐹:𝑉–1-1-onto→𝑊 ↔ 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) |
| 42 | 38 | raleqi 3324 |
. . . 4
⊢
(∀𝑣 ∈
𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))) ↔ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))) |
| 43 | 41, 42 | anbi12i 628 |
. . 3
⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))) ↔ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))))) |
| 44 | 37, 43 | bitr4di 289 |
. 2
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ {𝑓 ∣ (𝑓:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))} ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |
| 45 | 28, 44 | bitrd 279 |
1
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |