Theorem dfgric2

Description: Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

	Ref	Expression
Hypotheses	dfgric2.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	dfgric2.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	dfgric2.i	⊢ 𝐼 = ( iEdg ‘ 𝐴 )
	dfgric2.j	⊢ 𝐽 = ( iEdg ‘ 𝐵 )
Assertion	dfgric2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgric2.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		dfgric2.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		dfgric2.i	⊢ 𝐼 = ( iEdg ‘ 𝐴 )
4		dfgric2.j	⊢ 𝐽 = ( iEdg ‘ 𝐵 )
5		brgric	⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ( 𝐴 GraphIso 𝐵 ) ≠ ∅ )
6		n0	⊢ ( ( 𝐴 GraphIso 𝐵 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
7	5 6	bitri	⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
8		vex	⊢ 𝑓 ∈ V
9	1 2 3 4	isgrim	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ) ) )
10		eqcom	⊢ ( ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
11	10	ralbii	⊢ ( ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
12	11	anbi2i	⊢ ( ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
13	12	exbii	⊢ ( ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
14	13	anbi2i	⊢ ( ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
15	9 14	bitrdi	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
16	8 15	mp3an3	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
17	16	exbidv	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
18	7 17	bitrid	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )