Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ushrisomgr Structured version   Visualization version   GIF version
Theorem ushrisomgr 46495
Description: A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.)
Hypotheses
Ref Expression
ushrisomgr.v 𝑉 = (Vtxβ€˜πΊ)
ushrisomgr.e 𝐸 = (Edgβ€˜πΊ)
ushrisomgr.s 𝐻 = βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩
Assertion
Ref Expression
ushrisomgr (𝐺 ∈ USHGraph β†’ 𝐺 IsomGr 𝐻)
Proof of Theorem ushrisomgr
Dummy variables 𝑓 𝑔 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ushrisomgr.v . . . . . 6 𝑉 = (Vtxβ€˜πΊ)
21fvexi 6902 . . . . 5 𝑉 ∈ V
32a1i 11 . . . 4 (𝐺 ∈ USHGraph β†’ 𝑉 ∈ V)
43resiexd 7214 . . 3 (𝐺 ∈ USHGraph β†’ ( I β†Ύ 𝑉) ∈ V)
5 f1oi 6868 . . . . . 6 ( I β†Ύ 𝑉):𝑉–1-1-onto→𝑉
65a1i 11 . . . . 5 (𝐺 ∈ USHGraph β†’ ( I β†Ύ 𝑉):𝑉–1-1-onto→𝑉)
7 ushrisomgr.s . . . . . . . 8 𝐻 = βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩
87fveq2i 6891 . . . . . . 7 (Vtxβ€˜π») = (Vtxβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩)
9 ushrisomgr.e . . . . . . . . . . 11 𝐸 = (Edgβ€˜πΊ)
109fvexi 6902 . . . . . . . . . 10 𝐸 ∈ V
11 id 22 . . . . . . . . . . 11 (𝐸 ∈ V β†’ 𝐸 ∈ V)
1211resiexd 7214 . . . . . . . . . 10 (𝐸 ∈ V β†’ ( I β†Ύ 𝐸) ∈ V)
1310, 12ax-mp 5 . . . . . . . . 9 ( I β†Ύ 𝐸) ∈ V
142, 13pm3.2i 471 . . . . . . . 8 (𝑉 ∈ V ∧ ( I β†Ύ 𝐸) ∈ V)
15 opvtxfv 28253 . . . . . . . 8 ((𝑉 ∈ V ∧ ( I β†Ύ 𝐸) ∈ V) β†’ (Vtxβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩) = 𝑉)
1614, 15mp1i 13 . . . . . . 7 (𝐺 ∈ USHGraph β†’ (Vtxβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩) = 𝑉)
178, 16eqtrid 2784 . . . . . 6 (𝐺 ∈ USHGraph β†’ (Vtxβ€˜π») = 𝑉)
1817f1oeq3d 6827 . . . . 5 (𝐺 ∈ USHGraph β†’ (( I β†Ύ 𝑉):𝑉–1-1-ontoβ†’(Vtxβ€˜π») ↔ ( I β†Ύ 𝑉):𝑉–1-1-onto→𝑉))
196, 18mpbird 256 . . . 4 (𝐺 ∈ USHGraph β†’ ( I β†Ύ 𝑉):𝑉–1-1-ontoβ†’(Vtxβ€˜π»))
20 fvexd 6903 . . . . 5 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜πΊ) ∈ V)
21 eqid 2732 . . . . . . . . 9 (iEdgβ€˜πΊ) = (iEdgβ€˜πΊ)
221, 21ushgrf 28312 . . . . . . . 8 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1β†’(𝒫 𝑉 βˆ– {βˆ…}))
23 f1f1orn 6841 . . . . . . . 8 ((iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1β†’(𝒫 𝑉 βˆ– {βˆ…}) β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’ran (iEdgβ€˜πΊ))
2422, 23syl 17 . . . . . . 7 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’ran (iEdgβ€˜πΊ))
257fveq2i 6891 . . . . . . . . . . 11 (iEdgβ€˜π») = (iEdgβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩)
2610a1i 11 . . . . . . . . . . . . 13 (𝐺 ∈ USHGraph β†’ 𝐸 ∈ V)
2726resiexd 7214 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph β†’ ( I β†Ύ 𝐸) ∈ V)
28 opiedgfv 28256 . . . . . . . . . . . 12 ((𝑉 ∈ V ∧ ( I β†Ύ 𝐸) ∈ V) β†’ (iEdgβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩) = ( I β†Ύ 𝐸))
292, 27, 28sylancr 587 . . . . . . . . . . 11 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩) = ( I β†Ύ 𝐸))
3025, 29eqtrid 2784 . . . . . . . . . 10 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜π») = ( I β†Ύ 𝐸))
3130dmeqd 5903 . . . . . . . . 9 (𝐺 ∈ USHGraph β†’ dom (iEdgβ€˜π») = dom ( I β†Ύ 𝐸))
32 dmresi 6049 . . . . . . . . . 10 dom ( I β†Ύ 𝐸) = 𝐸
339a1i 11 . . . . . . . . . . 11 (𝐺 ∈ USHGraph β†’ 𝐸 = (Edgβ€˜πΊ))
34 edgval 28298 . . . . . . . . . . 11 (Edgβ€˜πΊ) = ran (iEdgβ€˜πΊ)
3533, 34eqtrdi 2788 . . . . . . . . . 10 (𝐺 ∈ USHGraph β†’ 𝐸 = ran (iEdgβ€˜πΊ))
3632, 35eqtrid 2784 . . . . . . . . 9 (𝐺 ∈ USHGraph β†’ dom ( I β†Ύ 𝐸) = ran (iEdgβ€˜πΊ))
3731, 36eqtrd 2772 . . . . . . . 8 (𝐺 ∈ USHGraph β†’ dom (iEdgβ€˜π») = ran (iEdgβ€˜πΊ))
3837f1oeq3d 6827 . . . . . . 7 (𝐺 ∈ USHGraph β†’ ((iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ↔ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’ran (iEdgβ€˜πΊ)))
3924, 38mpbird 256 . . . . . 6 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π»))
40 ushgruhgr 28318 . . . . . . . . . 10 (𝐺 ∈ USHGraph β†’ 𝐺 ∈ UHGraph)
411, 21uhgrss 28313 . . . . . . . . . 10 ((𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ((iEdgβ€˜πΊ)β€˜π‘–) βŠ† 𝑉)
4240, 41sylan 580 . . . . . . . . 9 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ((iEdgβ€˜πΊ)β€˜π‘–) βŠ† 𝑉)
43 resiima 6072 . . . . . . . . 9 (((iEdgβ€˜πΊ)β€˜π‘–) βŠ† 𝑉 β†’ (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜πΊ)β€˜π‘–))
4442, 43syl 17 . . . . . . . 8 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜πΊ)β€˜π‘–))
45 f1f 6784 . . . . . . . . . . . . 13 ((iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1β†’(𝒫 𝑉 βˆ– {βˆ…}) β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)⟢(𝒫 𝑉 βˆ– {βˆ…}))
4622, 45syl 17 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph β†’ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)⟢(𝒫 𝑉 βˆ– {βˆ…}))
4746ffund 6718 . . . . . . . . . . 11 (𝐺 ∈ USHGraph β†’ Fun (iEdgβ€˜πΊ))
48 fvelrn 7075 . . . . . . . . . . 11 ((Fun (iEdgβ€˜πΊ) ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ((iEdgβ€˜πΊ)β€˜π‘–) ∈ ran (iEdgβ€˜πΊ))
4947, 48sylan 580 . . . . . . . . . 10 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ((iEdgβ€˜πΊ)β€˜π‘–) ∈ ran (iEdgβ€˜πΊ))
509, 34eqtri 2760 . . . . . . . . . 10 𝐸 = ran (iEdgβ€˜πΊ)
5149, 50eleqtrrdi 2844 . . . . . . . . 9 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ((iEdgβ€˜πΊ)β€˜π‘–) ∈ 𝐸)
52 fvresi 7167 . . . . . . . . 9 (((iEdgβ€˜πΊ)β€˜π‘–) ∈ 𝐸 β†’ (( I β†Ύ 𝐸)β€˜((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜πΊ)β€˜π‘–))
5351, 52syl 17 . . . . . . . 8 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ (( I β†Ύ 𝐸)β€˜((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜πΊ)β€˜π‘–))
5410a1i 11 . . . . . . . . . . . 12 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ 𝐸 ∈ V)
5554resiexd 7214 . . . . . . . . . . 11 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ( I β†Ύ 𝐸) ∈ V)
562, 55, 28sylancr 587 . . . . . . . . . 10 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ (iEdgβ€˜βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩) = ( I β†Ύ 𝐸))
5725, 56eqtr2id 2785 . . . . . . . . 9 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ ( I β†Ύ 𝐸) = (iEdgβ€˜π»))
5857fveq1d 6890 . . . . . . . 8 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ (( I β†Ύ 𝐸)β€˜((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–)))
5944, 53, 583eqtr2d 2778 . . . . . . 7 ((𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom (iEdgβ€˜πΊ)) β†’ (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–)))
6059ralrimiva 3146 . . . . . 6 (𝐺 ∈ USHGraph β†’ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–)))
6139, 60jca 512 . . . . 5 (𝐺 ∈ USHGraph β†’ ((iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–))))
62 f1oeq1 6818 . . . . . 6 (𝑔 = (iEdgβ€˜πΊ) β†’ (𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ↔ (iEdgβ€˜πΊ):dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π»)))
63 fveq1 6887 . . . . . . . . 9 (𝑔 = (iEdgβ€˜πΊ) β†’ (π‘”β€˜π‘–) = ((iEdgβ€˜πΊ)β€˜π‘–))
6463fveq2d 6892 . . . . . . . 8 (𝑔 = (iEdgβ€˜πΊ) β†’ ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–)))
6564eqeq2d 2743 . . . . . . 7 (𝑔 = (iEdgβ€˜πΊ) β†’ ((( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)) ↔ (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–))))
6665ralbidv 3177 . . . . . 6 (𝑔 = (iEdgβ€˜πΊ) β†’ (βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)) ↔ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜((iEdgβ€˜πΊ)β€˜π‘–))))
6762, 66anbi12d 631 . . . . 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β€˜πΊ)β€˜π‘–)))))
6820, 61, 67spcedv 3588 . . . 4 (𝐺 ∈ USHGraph β†’ βˆƒπ‘”(𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–))))
6919, 68jca 512 . . 3 (𝐺 ∈ USHGraph β†’ (( I β†Ύ 𝑉):𝑉–1-1-ontoβ†’(Vtxβ€˜π») ∧ βˆƒπ‘”(𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)))))
70 f1oeq1 6818 . . . 4 (𝑓 = ( I β†Ύ 𝑉) β†’ (𝑓:𝑉–1-1-ontoβ†’(Vtxβ€˜π») ↔ ( I β†Ύ 𝑉):𝑉–1-1-ontoβ†’(Vtxβ€˜π»)))
71 imaeq1 6052 . . . . . . . 8 (𝑓 = ( I β†Ύ 𝑉) β†’ (𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)))
7271eqeq1d 2734 . . . . . . 7 (𝑓 = ( I β†Ύ 𝑉) β†’ ((𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)) ↔ (( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–))))
7372ralbidv 3177 . . . . . 6 (𝑓 = ( I β†Ύ 𝑉) β†’ (βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)) ↔ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(( I β†Ύ 𝑉) β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–))))
7473anbi2d 629 . . . . 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β€˜π»)β€˜(π‘”β€˜π‘–)))))
7574exbidv 1924 . . . 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β€˜π»)β€˜(π‘”β€˜π‘–)))))
7670, 75anbi12d 631 . . 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β€˜π»)β€˜(π‘”β€˜π‘–))))))
774, 69, 76spcedv 3588 . 2 (𝐺 ∈ USHGraph β†’ βˆƒπ‘“(𝑓:𝑉–1-1-ontoβ†’(Vtxβ€˜π») ∧ βˆƒπ‘”(𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–)))))
78 opex 5463 . . . 4 βŸ¨π‘‰, ( I β†Ύ 𝐸)⟩ ∈ V
797, 78eqeltri 2829 . . 3 𝐻 ∈ V
80 eqid 2732 . . . 4 (Vtxβ€˜π») = (Vtxβ€˜π»)
81 eqid 2732 . . . 4 (iEdgβ€˜π») = (iEdgβ€˜π»)
821, 80, 21, 81isomgr 46477 . . 3 ((𝐺 ∈ USHGraph ∧ 𝐻 ∈ V) β†’ (𝐺 IsomGr 𝐻 ↔ βˆƒπ‘“(𝑓:𝑉–1-1-ontoβ†’(Vtxβ€˜π») ∧ βˆƒπ‘”(𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–))))))
8379, 82mpan2 689 . 2 (𝐺 ∈ USHGraph β†’ (𝐺 IsomGr 𝐻 ↔ βˆƒπ‘“(𝑓:𝑉–1-1-ontoβ†’(Vtxβ€˜π») ∧ βˆƒπ‘”(𝑔:dom (iEdgβ€˜πΊ)–1-1-ontoβ†’dom (iEdgβ€˜π») ∧ βˆ€π‘– ∈ dom (iEdgβ€˜πΊ)(𝑓 β€œ ((iEdgβ€˜πΊ)β€˜π‘–)) = ((iEdgβ€˜π»)β€˜(π‘”β€˜π‘–))))))
8477, 83mpbird 256 1 (𝐺 ∈ USHGraph β†’ 𝐺 IsomGr 𝐻)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆ€wral 3061  Vcvv 3474   βˆ– cdif 3944   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βŸ¨cop 4633   class class class wbr 5147   I cid 5572  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678  Fun wfun 6534  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  Vtxcvtx 28245  iEdgciedg 28246  Edgcedg 28296  UHGraphcuhgr 28305  USHGraphcushgr 28306   IsomGr cisomgr 46473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-1st 7971  df-2nd 7972  df-vtx 28247  df-iedg 28248  df-edg 28297  df-uhgr 28307  df-ushgr 28308  df-isomgr 46475
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator