| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ushggricedg.v | . . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) | 
| 2 | 1 | fvexi 6920 | . . . . 5
⊢ 𝑉 ∈ V | 
| 3 | 2 | a1i 11 | . . . 4
⊢ (𝐺 ∈ USHGraph → 𝑉 ∈ V) | 
| 4 | 3 | resiexd 7236 | . . 3
⊢ (𝐺 ∈ USHGraph → ( I
↾ 𝑉) ∈
V) | 
| 5 |  | f1oi 6886 | . . . . . 6
⊢ ( I
↾ 𝑉):𝑉–1-1-onto→𝑉 | 
| 6 | 5 | a1i 11 | . . . . 5
⊢ (𝐺 ∈ USHGraph → ( I
↾ 𝑉):𝑉–1-1-onto→𝑉) | 
| 7 |  | ushggricedg.s | . . . . . . . 8
⊢ 𝐻 = 〈𝑉, ( I ↾ 𝐸)〉 | 
| 8 | 7 | fveq2i 6909 | . . . . . . 7
⊢
(Vtx‘𝐻) =
(Vtx‘〈𝑉, ( I
↾ 𝐸)〉) | 
| 9 |  | ushggricedg.e | . . . . . . . . . . 11
⊢ 𝐸 = (Edg‘𝐺) | 
| 10 | 9 | fvexi 6920 | . . . . . . . . . 10
⊢ 𝐸 ∈ V | 
| 11 |  | resiexg 7934 | . . . . . . . . . 10
⊢ (𝐸 ∈ V → ( I ↾
𝐸) ∈
V) | 
| 12 | 10, 11 | ax-mp 5 | . . . . . . . . 9
⊢ ( I
↾ 𝐸) ∈
V | 
| 13 | 2, 12 | pm3.2i 470 | . . . . . . . 8
⊢ (𝑉 ∈ V ∧ ( I ↾
𝐸) ∈
V) | 
| 14 |  | opvtxfv 29021 | . . . . . . . 8
⊢ ((𝑉 ∈ V ∧ ( I ↾
𝐸) ∈ V) →
(Vtx‘〈𝑉, ( I
↾ 𝐸)〉) = 𝑉) | 
| 15 | 13, 14 | mp1i 13 | . . . . . . 7
⊢ (𝐺 ∈ USHGraph →
(Vtx‘〈𝑉, ( I
↾ 𝐸)〉) = 𝑉) | 
| 16 | 8, 15 | eqtrid 2789 | . . . . . 6
⊢ (𝐺 ∈ USHGraph →
(Vtx‘𝐻) = 𝑉) | 
| 17 | 16 | f1oeq3d 6845 | . . . . 5
⊢ (𝐺 ∈ USHGraph → (( I
↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ↔ ( I ↾ 𝑉):𝑉–1-1-onto→𝑉)) | 
| 18 | 6, 17 | mpbird 257 | . . . 4
⊢ (𝐺 ∈ USHGraph → ( I
↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻)) | 
| 19 |  | fvexd 6921 | . . . . 5
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺) ∈
V) | 
| 20 |  | eqid 2737 | . . . . . . . . 9
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 21 | 1, 20 | ushgrf 29080 | . . . . . . . 8
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅})) | 
| 22 |  | f1f1orn 6859 | . . . . . . . 8
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→ran
(iEdg‘𝐺)) | 
| 23 | 21, 22 | syl 17 | . . . . . . 7
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→ran (iEdg‘𝐺)) | 
| 24 | 7 | fveq2i 6909 | . . . . . . . . . . 11
⊢
(iEdg‘𝐻) =
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) | 
| 25 | 10 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ USHGraph → 𝐸 ∈ V) | 
| 26 | 25 | resiexd 7236 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ USHGraph → ( I
↾ 𝐸) ∈
V) | 
| 27 |  | opiedgfv 29024 | . . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ ( I ↾
𝐸) ∈ V) →
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) = ( I
↾ 𝐸)) | 
| 28 | 2, 26, 27 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝐺 ∈ USHGraph →
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) = ( I
↾ 𝐸)) | 
| 29 | 24, 28 | eqtrid 2789 | . . . . . . . . . 10
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐻) = ( I
↾ 𝐸)) | 
| 30 | 29 | dmeqd 5916 | . . . . . . . . 9
⊢ (𝐺 ∈ USHGraph → dom
(iEdg‘𝐻) = dom ( I
↾ 𝐸)) | 
| 31 |  | dmresi 6070 | . . . . . . . . . 10
⊢ dom ( I
↾ 𝐸) = 𝐸 | 
| 32 | 9 | a1i 11 | . . . . . . . . . . 11
⊢ (𝐺 ∈ USHGraph → 𝐸 = (Edg‘𝐺)) | 
| 33 |  | edgval 29066 | . . . . . . . . . . 11
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) | 
| 34 | 32, 33 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺)) | 
| 35 | 31, 34 | eqtrid 2789 | . . . . . . . . 9
⊢ (𝐺 ∈ USHGraph → dom ( I
↾ 𝐸) = ran
(iEdg‘𝐺)) | 
| 36 | 30, 35 | eqtrd 2777 | . . . . . . . 8
⊢ (𝐺 ∈ USHGraph → dom
(iEdg‘𝐻) = ran
(iEdg‘𝐺)) | 
| 37 | 36 | f1oeq3d 6845 | . . . . . . 7
⊢ (𝐺 ∈ USHGraph →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→ran
(iEdg‘𝐺))) | 
| 38 | 23, 37 | mpbird 257 | . . . . . 6
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) | 
| 39 |  | ushgruhgr 29086 | . . . . . . . . . 10
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈
UHGraph) | 
| 40 | 1, 20 | uhgrss 29081 | . . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑉) | 
| 41 | 39, 40 | sylan 580 | . . . . . . . . 9
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ⊆ 𝑉) | 
| 42 |  | resiima 6094 | . . . . . . . . 9
⊢
(((iEdg‘𝐺)‘𝑖) ⊆ 𝑉 → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖)) | 
| 43 | 41, 42 | syl 17 | . . . . . . . 8
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖)) | 
| 44 |  | f1f 6804 | . . . . . . . . . . . . 13
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 𝑉 ∖
{∅})) | 
| 45 | 21, 44 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 𝑉 ∖ {∅})) | 
| 46 | 45 | ffund 6740 | . . . . . . . . . . 11
⊢ (𝐺 ∈ USHGraph → Fun
(iEdg‘𝐺)) | 
| 47 |  | fvelrn 7096 | . . . . . . . . . . 11
⊢ ((Fun
(iEdg‘𝐺) ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ ran (iEdg‘𝐺)) | 
| 48 | 46, 47 | sylan 580 | . . . . . . . . . 10
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ ran (iEdg‘𝐺)) | 
| 49 | 9, 33 | eqtri 2765 | . . . . . . . . . 10
⊢ 𝐸 = ran (iEdg‘𝐺) | 
| 50 | 48, 49 | eleqtrrdi 2852 | . . . . . . . . 9
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘𝑖) ∈ 𝐸) | 
| 51 |  | fvresi 7193 | . . . . . . . . 9
⊢
(((iEdg‘𝐺)‘𝑖) ∈ 𝐸 → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖)) | 
| 52 | 50, 51 | syl 17 | . . . . . . . 8
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐺)‘𝑖)) | 
| 53 | 10 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → 𝐸 ∈ V) | 
| 54 | 53 | resiexd 7236 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ( I ↾ 𝐸) ∈ V) | 
| 55 | 2, 54, 27 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) →
(iEdg‘〈𝑉, ( I
↾ 𝐸)〉) = ( I
↾ 𝐸)) | 
| 56 | 24, 55 | eqtr2id 2790 | . . . . . . . . 9
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → ( I ↾ 𝐸) = (iEdg‘𝐻)) | 
| 57 | 56 | fveq1d 6908 | . . . . . . . 8
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝐸)‘((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))) | 
| 58 | 43, 52, 57 | 3eqtr2d 2783 | . . . . . . 7
⊢ ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdg‘𝐺)) → (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))) | 
| 59 | 58 | ralrimiva 3146 | . . . . . 6
⊢ (𝐺 ∈ USHGraph →
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))) | 
| 60 | 38, 59 | jca 511 | . . . . 5
⊢ (𝐺 ∈ USHGraph →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))) | 
| 61 |  | f1oeq1 6836 | . . . . . 6
⊢ (𝑔 = (iEdg‘𝐺) → (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))) | 
| 62 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑔 = (iEdg‘𝐺) → (𝑔‘𝑖) = ((iEdg‘𝐺)‘𝑖)) | 
| 63 | 62 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑔 = (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑔‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))) | 
| 64 | 63 | eqeq2d 2748 | . . . . . . 7
⊢ (𝑔 = (iEdg‘𝐺) → ((( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))) | 
| 65 | 64 | ralbidv 3178 | . . . . . 6
⊢ (𝑔 = (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖)))) | 
| 66 | 61, 65 | anbi12d 632 | . . . . 5
⊢ (𝑔 = (iEdg‘𝐺) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘((iEdg‘𝐺)‘𝑖))))) | 
| 67 | 19, 60, 66 | spcedv 3598 | . . . 4
⊢ (𝐺 ∈ USHGraph →
∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))) | 
| 68 | 18, 67 | jca 511 | . . 3
⊢ (𝐺 ∈ USHGraph → (( I
↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))) | 
| 69 |  | f1oeq1 6836 | . . . 4
⊢ (𝑓 = ( I ↾ 𝑉) → (𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ↔ ( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻))) | 
| 70 |  | imaeq1 6073 | . . . . . . . 8
⊢ (𝑓 = ( I ↾ 𝑉) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖))) | 
| 71 | 70 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ (( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))) | 
| 72 | 71 | ralbidv 3178 | . . . . . 6
⊢ (𝑓 = ( I ↾ 𝑉) → (∀𝑖 ∈ dom (iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)(( I ↾ 𝑉) “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))) | 
| 73 | 72 | anbi2d 630 | . . . . 5
⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ (𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))) | 
| 74 | 73 | exbidv 1921 | . . . 4
⊢ (𝑓 = ( I ↾ 𝑉) → (∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))) ↔ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))) | 
| 75 | 69, 74 | anbi12d 632 | . . 3
⊢ (𝑓 = ( I ↾ 𝑉) → ((𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))) ↔ (( I ↾ 𝑉):𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(( I ↾
𝑉) “
((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))) | 
| 76 | 4, 68, 75 | spcedv 3598 | . 2
⊢ (𝐺 ∈ USHGraph →
∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖))))) | 
| 77 |  | opex 5469 | . . . 4
⊢
〈𝑉, ( I ↾
𝐸)〉 ∈
V | 
| 78 | 7, 77 | eqeltri 2837 | . . 3
⊢ 𝐻 ∈ V | 
| 79 |  | eqid 2737 | . . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) | 
| 80 |  | eqid 2737 | . . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) | 
| 81 | 1, 79, 20, 80 | dfgric2 47884 | . . 3
⊢ ((𝐺 ∈ USHGraph ∧ 𝐻 ∈ V) → (𝐺
≃𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))) | 
| 82 | 78, 81 | mpan2 691 | . 2
⊢ (𝐺 ∈ USHGraph → (𝐺
≃𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→(Vtx‘𝐻) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐺)–1-1-onto→dom
(iEdg‘𝐻) ∧
∀𝑖 ∈ dom
(iEdg‘𝐺)(𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(𝑔‘𝑖)))))) | 
| 83 | 76, 82 | mpbird 257 | 1
⊢ (𝐺 ∈ USHGraph → 𝐺
≃𝑔𝑟 𝐻) |