Theorem isomuspgrlem2

Description: Lemma 2 for isomuspgr . (Contributed by AV, 1-Dec-2022)

	Ref	Expression
Hypotheses	isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
	isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
Assertion	isomuspgrlem2	⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) → ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
4		isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
5	3	fvexi	⊢ 𝐸 ∈ V
6	5	mptex	⊢ ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ∈ V
7		eqid	⊢ ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) )
8		simplll	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → 𝐴 ∈ USPGraph )
9		simplr	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → 𝑓 : 𝑉 –1-1-onto→ 𝑊 )
10		simpr	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
11		vex	⊢ 𝑓 ∈ V
12	11	a1i	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → 𝑓 ∈ V )
13		simpllr	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → 𝐵 ∈ USPGraph )
14	1 2 3 4 7 8 9 10 12 13	isomuspgrlem2e	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐾 )
15	1 2 3 4 7	isomuspgrlem2a	⊢ ( 𝑓 ∈ V → ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) )
16	11 15	mp1i	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) )
17	14 16	jca	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) ) )
18		f1oeq1	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) → ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ↔ ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐾 ) )
19		fveq1	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) → ( 𝑔 ‘ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) )
20	19	eqeq2d	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) ) )
21	20	ralbidv	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) → ( ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) ) )
22	18 21	anbi12d	⊢ ( 𝑔 = ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) → ( ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) ) ) )
23	22	spcegv	⊢ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ∈ V → ( ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( ( 𝑥 ∈ 𝐸 ↦ ( 𝑓 “ 𝑥 ) ) ‘ 𝑒 ) ) → ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
24	6 17 23	mpsyl	⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) )
25	24	ex	⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) → ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )