Theorem isomgr

Description: The isomorphy relation for two graphs. (Contributed by AV, 11-Nov-2022)

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

Proof

Step	Hyp	Ref	Expression
1		isomgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomgr.i	⊢ 𝐼 = ( iEdg ‘ 𝐴 )
4		isomgr.j	⊢ 𝐽 = ( iEdg ‘ 𝐵 )
5		eqidd	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑓 = 𝑓 )
6		fveq2	⊢ ( 𝑥 = 𝐴 → ( Vtx ‘ 𝑥 ) = ( Vtx ‘ 𝐴 ) )
7	6	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( Vtx ‘ 𝑥 ) = ( Vtx ‘ 𝐴 ) )
8	7 1	eqtr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( Vtx ‘ 𝑥 ) = 𝑉 )
9		fveq2	⊢ ( 𝑦 = 𝐵 → ( Vtx ‘ 𝑦 ) = ( Vtx ‘ 𝐵 ) )
10	9	adantl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( Vtx ‘ 𝑦 ) = ( Vtx ‘ 𝐵 ) )
11	10 2	eqtr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( Vtx ‘ 𝑦 ) = 𝑊 )
12	5 8 11	f1oeq123d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ↔ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) )
13		eqidd	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑔 = 𝑔 )
14		fveq2	⊢ ( 𝑥 = 𝐴 → ( iEdg ‘ 𝑥 ) = ( iEdg ‘ 𝐴 ) )
15	14	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( iEdg ‘ 𝑥 ) = ( iEdg ‘ 𝐴 ) )
16	15 3	eqtr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( iEdg ‘ 𝑥 ) = 𝐼 )
17	16	dmeqd	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → dom ( iEdg ‘ 𝑥 ) = dom 𝐼 )
18		fveq2	⊢ ( 𝑦 = 𝐵 → ( iEdg ‘ 𝑦 ) = ( iEdg ‘ 𝐵 ) )
19	18	adantl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( iEdg ‘ 𝑦 ) = ( iEdg ‘ 𝐵 ) )
20	19 4	eqtr4di	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( iEdg ‘ 𝑦 ) = 𝐽 )
21	20	dmeqd	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → dom ( iEdg ‘ 𝑦 ) = dom 𝐽 )
22	13 17 21	f1oeq123d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ↔ 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ) )
23	16	fveq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) = ( 𝐼 ‘ 𝑖 ) )
24	23	imaeq2d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) )
25	20	fveq1d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
26	24 25	eqeq12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
27	17 26	raleqbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
28	22 27	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
29	28	exbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
30	12 29	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
31	30	exbidv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
32		df-isomgr	⊢ IsomGr = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) }
33	31 32	brabga	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )