Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isomgrsym Structured version   Visualization version   GIF version

Theorem isomgrsym 43994
 Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.)
Assertion
Ref Expression
isomgrsym ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝐴 IsomGr 𝐵𝐵 IsomGr 𝐴))

Proof of Theorem isomgrsym
Dummy variables 𝑒 𝑓 𝑔 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2821 . . 3 (Vtx‘𝐴) = (Vtx‘𝐴)
2 eqid 2821 . . 3 (Vtx‘𝐵) = (Vtx‘𝐵)
3 eqid 2821 . . 3 (iEdg‘𝐴) = (iEdg‘𝐴)
4 eqid 2821 . . 3 (iEdg‘𝐵) = (iEdg‘𝐵)
51, 2, 3, 4isomgr 43981 . 2 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))))
6 vex 3498 . . . . . . . 8 𝑓 ∈ V
76cnvex 7624 . . . . . . 7 𝑓 ∈ V
87a1i 11 . . . . . 6 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → 𝑓 ∈ V)
9 f1ocnv 6622 . . . . . . . . 9 (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → 𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴))
109adantr 483 . . . . . . . 8 ((𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)))) → 𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴))
1110adantl 484 . . . . . . 7 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → 𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴))
12 vex 3498 . . . . . . . . . . . . . 14 𝑔 ∈ V
1312cnvex 7624 . . . . . . . . . . . . 13 𝑔 ∈ V
1413a1i 11 . . . . . . . . . . . 12 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → 𝑔 ∈ V)
15 f1ocnv 6622 . . . . . . . . . . . . . . 15 (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → 𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴))
1615adantr 483 . . . . . . . . . . . . . 14 ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) → 𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴))
17163ad2ant2 1130 . . . . . . . . . . . . 13 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → 𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴))
18 f1ocnvdm 7035 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔𝑗) ∈ dom (iEdg‘𝐴))
19183ad2antl2 1182 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔𝑗) ∈ dom (iEdg‘𝐴))
20 fveq2 6665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = (𝑔𝑗) → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘(𝑔𝑗)))
2120imaeq2d 5924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = (𝑔𝑗) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))))
22 2fveq3 6670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = (𝑔𝑗) → ((iEdg‘𝐵)‘(𝑔𝑖)) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗))))
2321, 22eqeq12d 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = (𝑔𝑗) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗)))))
2423adantl 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ 𝑖 = (𝑔𝑗)) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗)))))
2519, 24rspcdv 3615 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗)))))
26 f1ocnvfv2 7028 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔‘(𝑔𝑗)) = 𝑗)
27263ad2antl2 1182 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑔‘(𝑔𝑗)) = 𝑗)
2827fveq2d 6669 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗))
2928eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗))) ↔ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗)))
30 f1of1 6609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵))
31303ad2ant3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵))
3231adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → 𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵))
33 simpl1l 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → 𝐴 ∈ UHGraph)
341, 3uhgrss 26843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ UHGraph ∧ (𝑔𝑗) ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘(𝑔𝑗)) ⊆ (Vtx‘𝐴))
3533, 19, 34syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐴)‘(𝑔𝑗)) ⊆ (Vtx‘𝐴))
3632, 35jca 514 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(𝑔𝑗)) ⊆ (Vtx‘𝐴)))
3736adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(𝑔𝑗)) ⊆ (Vtx‘𝐴)))
38 f1imacnv 6626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:(Vtx‘𝐴)–1-1→(Vtx‘𝐵) ∧ ((iEdg‘𝐴)‘(𝑔𝑗)) ⊆ (Vtx‘𝐴)) → (𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗)))) = ((iEdg‘𝐴)‘(𝑔𝑗)))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗)))) = ((iEdg‘𝐴)‘(𝑔𝑗)))
40 imaeq2 5920 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗) → (𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗)))) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))
4140adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗)) → (𝑓 “ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗)))) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))
4239, 41eqtr3d 2858 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) ∧ (𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗)) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))
4342ex 415 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘𝑗) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗))))
4429, 43sylbid 242 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((𝑓 “ ((iEdg‘𝐴)‘(𝑔𝑗))) = ((iEdg‘𝐵)‘(𝑔‘(𝑔𝑗))) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗))))
4525, 44syld 47 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗))))
4645ex 415 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (𝑗 ∈ dom (iEdg‘𝐵) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))))
4746com23 86 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ 𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))))
48473exp 1115 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))))))
4948com34 91 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))))))
5049impd 413 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (𝑗 ∈ dom (iEdg‘𝐵) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗))))))
51503imp1 1343 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → ((iEdg‘𝐴)‘(𝑔𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))
5251eqcomd 2827 . . . . . . . . . . . . . 14 ((((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) ∧ 𝑗 ∈ dom (iEdg‘𝐵)) → (𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗)))
5352ralrimiva 3182 . . . . . . . . . . . . 13 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗)))
5417, 53jca 514 . . . . . . . . . . . 12 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → (𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗))))
55 f1oeq1 6599 . . . . . . . . . . . . 13 ( = 𝑔 → (:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ↔ 𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴)))
56 fveq1 6664 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (𝑗) = (𝑔𝑗))
5756fveq2d 6669 . . . . . . . . . . . . . . 15 ( = 𝑔 → ((iEdg‘𝐴)‘(𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗)))
5857eqeq2d 2832 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)) ↔ (𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗))))
5958ralbidv 3197 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)) ↔ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗))))
6055, 59anbi12d 632 . . . . . . . . . . . 12 ( = 𝑔 → ((:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))) ↔ (𝑔:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑔𝑗)))))
6114, 54, 60spcedv 3599 . . . . . . . . . . 11 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) ∧ 𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵)) → ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))
62613exp 1115 . . . . . . . . . 10 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → ((𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
6362exlimdv 1930 . . . . . . . . 9 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
6463com23 86 . . . . . . . 8 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) → (∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))) → ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
6564imp32 421 . . . . . . 7 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))
6611, 65jca 514 . . . . . 6 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → (𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)))))
67 f1oeq1 6599 . . . . . . 7 (𝑒 = 𝑓 → (𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ↔ 𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴)))
68 imaeq1 5919 . . . . . . . . . . 11 (𝑒 = 𝑓 → (𝑒 “ ((iEdg‘𝐵)‘𝑗)) = (𝑓 “ ((iEdg‘𝐵)‘𝑗)))
6968eqeq1d 2823 . . . . . . . . . 10 (𝑒 = 𝑓 → ((𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)) ↔ (𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))
7069ralbidv 3197 . . . . . . . . 9 (𝑒 = 𝑓 → (∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)) ↔ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))
7170anbi2d 630 . . . . . . . 8 (𝑒 = 𝑓 → ((:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))) ↔ (:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)))))
7271exbidv 1918 . . . . . . 7 (𝑒 = 𝑓 → (∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))) ↔ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)))))
7367, 72anbi12d 632 . . . . . 6 (𝑒 = 𝑓 → ((𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)))) ↔ (𝑓:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑓 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
748, 66, 73spcedv 3599 . . . . 5 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗)))))
752, 1, 4, 3isomgr 43981 . . . . . . 7 ((𝐵𝑌𝐴 ∈ UHGraph) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
7675ancoms 461 . . . . . 6 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
7776adantr 483 . . . . 5 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → (𝐵 IsomGr 𝐴 ↔ ∃𝑒(𝑒:(Vtx‘𝐵)–1-1-onto→(Vtx‘𝐴) ∧ ∃(:dom (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐴) ∧ ∀𝑗 ∈ dom (iEdg‘𝐵)(𝑒 “ ((iEdg‘𝐵)‘𝑗)) = ((iEdg‘𝐴)‘(𝑗))))))
7874, 77mpbird 259 . . . 4 (((𝐴 ∈ UHGraph ∧ 𝐵𝑌) ∧ (𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖))))) → 𝐵 IsomGr 𝐴)
7978ex 415 . . 3 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → ((𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)))) → 𝐵 IsomGr 𝐴))
8079exlimdv 1930 . 2 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (∃𝑓(𝑓:(Vtx‘𝐴)–1-1-onto→(Vtx‘𝐵) ∧ ∃𝑔(𝑔:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑔𝑖)))) → 𝐵 IsomGr 𝐴))
815, 80sylbid 242 1 ((𝐴 ∈ UHGraph ∧ 𝐵𝑌) → (𝐴 IsomGr 𝐵𝐵 IsomGr 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ∀wral 3138  Vcvv 3495   ⊆ wss 3936   class class class wbr 5059  ◡ccnv 5549  dom cdm 5550   “ cima 5553  –1-1→wf1 6347  –1-1-onto→wf1o 6349  ‘cfv 6350  Vtxcvtx 26775  iEdgciedg 26776  UHGraphcuhgr 26835   IsomGr cisomgr 43977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-uhgr 26837  df-isomgr 43979 This theorem is referenced by:  isomgrsymb  43995
 Copyright terms: Public domain W3C validator