Theorem isomgrsymb

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

	Ref	Expression
Assertion	isomgrsymb	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 IsomGr 𝐵 ↔ 𝐵 IsomGr 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isomgrsym	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 IsomGr 𝐵 → 𝐵 IsomGr 𝐴 ) )
2		isomgrsym	⊢ ( ( 𝐵 ∈ UHGraph ∧ 𝐴 ∈ UHGraph ) → ( 𝐵 IsomGr 𝐴 → 𝐴 IsomGr 𝐵 ) )
3	2	ancoms	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐵 IsomGr 𝐴 → 𝐴 IsomGr 𝐵 ) )
4	1 3	impbid	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 IsomGr 𝐵 ↔ 𝐵 IsomGr 𝐴 ) )