Metamath Proof Explorer

Theorem isomuspgr

Description: The isomorphy relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (Contributed by AV, 1-Dec-2022)

Ref Expression
Hypotheses isomushgr.v ⊢V=Vtx⁡A
isomushgr.w ⊢W=Vtx⁡B
isomushgr.e ⊢E=Edg⁡A
isomushgr.k ⊢K=Edg⁡B
Assertion isomuspgr ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K

Proof

Step Hyp Ref Expression
1 isomushgr.v ⊢V=Vtx⁡A
2 isomushgr.w ⊢W=Vtx⁡B
3 isomushgr.e ⊢E=Edg⁡A
4 isomushgr.k ⊢K=Edg⁡B
5 uspgrushgr ⊢A∈USHGraph→A∈USHGraph
6 uspgrushgr ⊢B∈USHGraph→B∈USHGraph
7 1 2 3 4 isomushgr ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
8 5 6 7 syl2an ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
9 imaeq2 ⊢e=ab→fe=fab
10 fveq2 ⊢e=ab→g⁡e=g⁡ab
11 9 10 eqeq12d ⊢e=ab→fe=g⁡e↔fab=g⁡ab
12 11 rspccv ⊢∀e∈Efe=g⁡e→ab∈E→fab=g⁡ab
13 12 adantl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e→ab∈E→fab=g⁡ab
14 13 imp ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→fab=g⁡ab
15 f1ofn ⊢f:V⟶1-1 ontoW→fFnV
16 15 ad3antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V→fFnV
17 simprl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V→a∈V
18 simprr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V→b∈V
19 fnimapr ⊢fFnV∧a∈V∧b∈V→fab=f⁡af⁡b
20 16 17 18 19 syl3anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V→fab=f⁡af⁡b
21 20 eqeq1d ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V→fab=g⁡ab↔f⁡af⁡b=g⁡ab
22 21 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e→fab=g⁡ab↔f⁡af⁡b=g⁡ab
23 22 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→fab=g⁡ab↔f⁡af⁡b=g⁡ab
24 f1of ⊢g:E⟶1-1 ontoK→g:E⟶K
25 24 ad3antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e→g:E⟶K
26 25 ffvelcdmda ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→g⁡ab∈K
27 eleq1 ⊢f⁡af⁡b=g⁡ab→f⁡af⁡b∈K↔g⁡ab∈K
28 26 27 syl5ibrcom ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→f⁡af⁡b=g⁡ab→f⁡af⁡b∈K
29 23 28 sylbid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→fab=g⁡ab→f⁡af⁡b∈K
30 14 29 mpd ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧a∈V∧b∈V∧∀e∈Efe=g⁡e∧ab∈E→f⁡af⁡b∈K
31 30 exp41 ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK→a∈V∧b∈V→∀e∈Efe=g⁡e→ab∈E→f⁡af⁡b∈K
32 31 com23 ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK→∀e∈Efe=g⁡e→a∈V∧b∈V→ab∈E→f⁡af⁡b∈K
33 32 impr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→a∈V∧b∈V→ab∈E→f⁡af⁡b∈K
34 33 imp ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧a∈V∧b∈V→ab∈E→f⁡af⁡b∈K
35 1 2 3 4 isomuspgrlem1 ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧a∈V∧b∈V→f⁡af⁡b∈K→ab∈E
36 34 35 impbid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧a∈V∧b∈V→ab∈E↔f⁡af⁡b∈K
37 36 ralrimivva ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
38 37 ex ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
39 38 exlimdv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
40 1 2 3 4 isomuspgrlem2 ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
41 39 40 impbid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e↔∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
42 41 pm5.32da ⊢A∈USHGraph∧B∈USHGraph→f:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e↔f:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
43 42 exbidv ⊢A∈USHGraph∧B∈USHGraph→∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e↔∃ff:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K
44 8 43 bitrd ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∀a∈V∀b∈Vab∈E↔f⁡af⁡b∈K