Theorem isomuspgrlem2c

Description: Lemma 3 for isomuspgrlem2 . (Contributed by AV, 29-Nov-2022)

	Ref	Expression
Hypotheses	isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
	isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
	isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
	isomuspgrlem2.a	⊢ ( 𝜑 → 𝐴 ∈ USPGraph )
	isomuspgrlem2.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
	isomuspgrlem2.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
	isomuspgrlem2.x	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
Assertion	isomuspgrlem2c	⊢ ( 𝜑 → 𝐺 : 𝐸 –1-1→ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomushgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomushgr.e	⊢ 𝐸 = ( Edg ‘ 𝐴 )
4		isomushgr.k	⊢ 𝐾 = ( Edg ‘ 𝐵 )
5		isomuspgrlem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
6		isomuspgrlem2.a	⊢ ( 𝜑 → 𝐴 ∈ USPGraph )
7		isomuspgrlem2.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
8		isomuspgrlem2.i	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
9		isomuspgrlem2.x	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
10	1 2 3 4 5 6 7 8	isomuspgrlem2b	⊢ ( 𝜑 → 𝐺 : 𝐸 ⟶ 𝐾 )
11	1 2 3 4 5	isomuspgrlem2a	⊢ ( 𝐹 ∈ 𝑋 → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )
12	9 11	syl	⊢ ( 𝜑 → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )
13		imaeq2	⊢ ( 𝑒 = 𝑐 → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ 𝑐 ) )
14		fveq2	⊢ ( 𝑒 = 𝑐 → ( 𝐺 ‘ 𝑒 ) = ( 𝐺 ‘ 𝑐 ) )
15	13 14	eqeq12d	⊢ ( 𝑒 = 𝑐 → ( ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ↔ ( 𝐹 “ 𝑐 ) = ( 𝐺 ‘ 𝑐 ) ) )
16	15	rspcv	⊢ ( 𝑐 ∈ 𝐸 → ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) → ( 𝐹 “ 𝑐 ) = ( 𝐺 ‘ 𝑐 ) ) )
17	16	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) → ( 𝐹 “ 𝑐 ) = ( 𝐺 ‘ 𝑐 ) ) )
18	17	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) → ( 𝐹 “ 𝑐 ) = ( 𝐺 ‘ 𝑐 ) )
19	18	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) → ( 𝐺 ‘ 𝑐 ) = ( 𝐹 “ 𝑐 ) )
20		imaeq2	⊢ ( 𝑒 = 𝑑 → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ 𝑑 ) )
21		fveq2	⊢ ( 𝑒 = 𝑑 → ( 𝐺 ‘ 𝑒 ) = ( 𝐺 ‘ 𝑑 ) )
22	20 21	eqeq12d	⊢ ( 𝑒 = 𝑑 → ( ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ↔ ( 𝐹 “ 𝑑 ) = ( 𝐺 ‘ 𝑑 ) ) )
23	22	rspcv	⊢ ( 𝑑 ∈ 𝐸 → ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) → ( 𝐹 “ 𝑑 ) = ( 𝐺 ‘ 𝑑 ) ) )
24	23	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) → ( 𝐹 “ 𝑑 ) = ( 𝐺 ‘ 𝑑 ) ) )
25	24	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) → ( 𝐹 “ 𝑑 ) = ( 𝐺 ‘ 𝑑 ) )
26	25	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) → ( 𝐺 ‘ 𝑑 ) = ( 𝐹 “ 𝑑 ) )
27	19 26	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) → ( ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑑 ) ↔ ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑑 ) ) )
28	12 27	mpidan	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑑 ) ↔ ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑑 ) ) )
29		f1of1	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
30	7 29	syl	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1→ 𝑊 )
31		uspgrupgr	⊢ ( 𝐴 ∈ USPGraph → 𝐴 ∈ UPGraph )
32		upgruhgr	⊢ ( 𝐴 ∈ UPGraph → 𝐴 ∈ UHGraph )
33	3	eleq2i	⊢ ( 𝑐 ∈ 𝐸 ↔ 𝑐 ∈ ( Edg ‘ 𝐴 ) )
34		edguhgr	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝑐 ∈ ( Edg ‘ 𝐴 ) ) → 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) )
35		elpwi	⊢ ( 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑐 ⊆ ( Vtx ‘ 𝐴 ) )
36	35 1	sseqtrrdi	⊢ ( 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑐 ⊆ 𝑉 )
37	34 36	syl	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝑐 ∈ ( Edg ‘ 𝐴 ) ) → 𝑐 ⊆ 𝑉 )
38	37	ex	⊢ ( 𝐴 ∈ UHGraph → ( 𝑐 ∈ ( Edg ‘ 𝐴 ) → 𝑐 ⊆ 𝑉 ) )
39	33 38	syl5bi	⊢ ( 𝐴 ∈ UHGraph → ( 𝑐 ∈ 𝐸 → 𝑐 ⊆ 𝑉 ) )
40	3	eleq2i	⊢ ( 𝑑 ∈ 𝐸 ↔ 𝑑 ∈ ( Edg ‘ 𝐴 ) )
41		edguhgr	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝑑 ∈ ( Edg ‘ 𝐴 ) ) → 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) )
42		elpwi	⊢ ( 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑑 ⊆ ( Vtx ‘ 𝐴 ) )
43	42 1	sseqtrrdi	⊢ ( 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑑 ⊆ 𝑉 )
44	41 43	syl	⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝑑 ∈ ( Edg ‘ 𝐴 ) ) → 𝑑 ⊆ 𝑉 )
45	44	ex	⊢ ( 𝐴 ∈ UHGraph → ( 𝑑 ∈ ( Edg ‘ 𝐴 ) → 𝑑 ⊆ 𝑉 ) )
46	40 45	syl5bi	⊢ ( 𝐴 ∈ UHGraph → ( 𝑑 ∈ 𝐸 → 𝑑 ⊆ 𝑉 ) )
47	39 46	anim12d	⊢ ( 𝐴 ∈ UHGraph → ( ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ⊆ 𝑉 ∧ 𝑑 ⊆ 𝑉 ) ) )
48	32 47	syl	⊢ ( 𝐴 ∈ UPGraph → ( ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ⊆ 𝑉 ∧ 𝑑 ⊆ 𝑉 ) ) )
49	6 31 48	3syl	⊢ ( 𝜑 → ( ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ⊆ 𝑉 ∧ 𝑑 ⊆ 𝑉 ) ) )
50	49	imp	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( 𝑐 ⊆ 𝑉 ∧ 𝑑 ⊆ 𝑉 ) )
51		f1imaeq	⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( 𝑐 ⊆ 𝑉 ∧ 𝑑 ⊆ 𝑉 ) ) → ( ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑑 ) ↔ 𝑐 = 𝑑 ) )
52	30 50 51	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑑 ) ↔ 𝑐 = 𝑑 ) )
53	52	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑑 ) → 𝑐 = 𝑑 ) )
54	28 53	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
55	54	ralrimivva	⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐸 ∀ 𝑑 ∈ 𝐸 ( ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
56		dff13	⊢ ( 𝐺 : 𝐸 –1-1→ 𝐾 ↔ ( 𝐺 : 𝐸 ⟶ 𝐾 ∧ ∀ 𝑐 ∈ 𝐸 ∀ 𝑑 ∈ 𝐸 ( ( 𝐺 ‘ 𝑐 ) = ( 𝐺 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) )
57	10 55 56	sylanbrc	⊢ ( 𝜑 → 𝐺 : 𝐸 –1-1→ 𝐾 )