isomuspgrlem2d

	Ref	Expression
Hypotheses	isomushgr.v	$⊢ V = Vtx (A)$
	isomushgr.w	$⊢ W = Vtx (B)$
	isomushgr.e	$⊢ E = Edg (A)$
	isomushgr.k	$⊢ K = Edg (B)$
	isomuspgrlem2.g	$⊢ G = (x \in E ⟼ F [x])$
	isomuspgrlem2.a	$⊢ φ \to A \in USHGraph$
	isomuspgrlem2.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} W$
	isomuspgrlem2.i	$⊢ φ \to \forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K)$
	isomuspgrlem2.x	$⊢ φ \to F \in X$
	isomuspgrlem2.b	$⊢ φ \to B \in USHGraph$
Assertion	isomuspgrlem2d	$⊢ φ \to G : E \underset{onto}{⟶} K$

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	$⊢ V = Vtx (A)$
2		isomushgr.w	$⊢ W = Vtx (B)$
3		isomushgr.e	$⊢ E = Edg (A)$
4		isomushgr.k	$⊢ K = Edg (B)$
5		isomuspgrlem2.g	$⊢ G = (x \in E ⟼ F [x])$
6		isomuspgrlem2.a	$⊢ φ \to A \in USHGraph$
7		isomuspgrlem2.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} W$
8		isomuspgrlem2.i	$⊢ φ \to \forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K)$
9		isomuspgrlem2.x	$⊢ φ \to F \in X$
10		isomuspgrlem2.b	$⊢ φ \to B \in USHGraph$
11	1 2 3 4 5 6 7 8	isomuspgrlem2b	$⊢ φ \to G : E ⟶ K$
12		uspgrupgr	$⊢ B \in USHGraph \to B \in UPGraph$
13	10 12	syl	$⊢ φ \to B \in UPGraph$
14	2 4	upgredg	$⊢ (B \in UPGraph \land y \in K) \to \exists c \in W \exists d \in W y = \{c, d\}$
15	13 14	sylan	$⊢ (φ \land y \in K) \to \exists c \in W \exists d \in W y = \{c, d\}$
16		eleq1	$⊢ y = \{c, d\} \to (y \in K \leftrightarrow \{c, d\} \in K)$
17	16	anbi2d	$⊢ y = \{c, d\} \to ((φ \land y \in K) \leftrightarrow (φ \land \{c, d\} \in K))$
18		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} W \to F : V \underset{onto}{⟶} W$
19	7 18	syl	$⊢ φ \to F : V \underset{onto}{⟶} W$
20		foelrn	$⊢ (F : V \underset{onto}{⟶} W \land c \in W) \to \exists m \in V c = F (m)$
21	19 20	sylan	$⊢ (φ \land c \in W) \to \exists m \in V c = F (m)$
22	21	ex	$⊢ φ \to (c \in W \to \exists m \in V c = F (m))$
23		foelrn	$⊢ (F : V \underset{onto}{⟶} W \land d \in W) \to \exists n \in V d = F (n)$
24	19 23	sylan	$⊢ (φ \land d \in W) \to \exists n \in V d = F (n)$
25	24	ex	$⊢ φ \to (d \in W \to \exists n \in V d = F (n))$
26	22 25	anim12d	$⊢ φ \to ((c \in W \land d \in W) \to (\exists m \in V c = F (m) \land \exists n \in V d = F (n)))$
27	26	adantr	$⊢ (φ \land \{c, d\} \in K) \to ((c \in W \land d \in W) \to (\exists m \in V c = F (m) \land \exists n \in V d = F (n)))$
28	27	imp	$⊢ ((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \to (\exists m \in V c = F (m) \land \exists n \in V d = F (n))$
29		preq12	$⊢ (c = F (m) \land d = F (n)) \to \{c, d\} = \{F (m), F (n)\}$
30	29	ancoms	$⊢ (d = F (n) \land c = F (m)) \to \{c, d\} = \{F (m), F (n)\}$
31	30	eleq1d	$⊢ (d = F (n) \land c = F (m)) \to (\{c, d\} \in K \leftrightarrow \{F (m), F (n)\} \in K)$
32		preq1	$⊢ a = m \to \{a, b\} = \{m, b\}$
33	32	eleq1d	$⊢ a = m \to (\{a, b\} \in E \leftrightarrow \{m, b\} \in E)$
34		fveq2	$⊢ a = m \to F (a) = F (m)$
35	34	preq1d	$⊢ a = m \to \{F (a), F (b)\} = \{F (m), F (b)\}$
36	35	eleq1d	$⊢ a = m \to (\{F (a), F (b)\} \in K \leftrightarrow \{F (m), F (b)\} \in K)$
37	33 36	bibi12d	$⊢ a = m \to ((\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K) \leftrightarrow (\{m, b\} \in E \leftrightarrow \{F (m), F (b)\} \in K))$
38		preq2	$⊢ b = n \to \{m, b\} = \{m, n\}$
39	38	eleq1d	$⊢ b = n \to (\{m, b\} \in E \leftrightarrow \{m, n\} \in E)$
40		fveq2	$⊢ b = n \to F (b) = F (n)$
41	40	preq2d	$⊢ b = n \to \{F (m), F (b)\} = \{F (m), F (n)\}$
42	41	eleq1d	$⊢ b = n \to (\{F (m), F (b)\} \in K \leftrightarrow \{F (m), F (n)\} \in K)$
43	39 42	bibi12d	$⊢ b = n \to ((\{m, b\} \in E \leftrightarrow \{F (m), F (b)\} \in K) \leftrightarrow (\{m, n\} \in E \leftrightarrow \{F (m), F (n)\} \in K))$
44	37 43	rspc2va	$⊢ ((m \in V \land n \in V) \land \forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K)) \to (\{m, n\} \in E \leftrightarrow \{F (m), F (n)\} \in K)$
45	44	bicomd	$⊢ ((m \in V \land n \in V) \land \forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K)) \to (\{F (m), F (n)\} \in K \leftrightarrow \{m, n\} \in E)$
46	45	ancoms	$⊢ (\forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K) \land (m \in V \land n \in V)) \to (\{F (m), F (n)\} \in K \leftrightarrow \{m, n\} \in E)$
47	46	biimpd	$⊢ (\forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K) \land (m \in V \land n \in V)) \to (\{F (m), F (n)\} \in K \to \{m, n\} \in E)$
48	47	ex	$⊢ \forall a \in V \forall b \in V (\{a, b\} \in E \leftrightarrow \{F (a), F (b)\} \in K) \to ((m \in V \land n \in V) \to (\{F (m), F (n)\} \in K \to \{m, n\} \in E))$
49	8 48	syl	$⊢ φ \to ((m \in V \land n \in V) \to (\{F (m), F (n)\} \in K \to \{m, n\} \in E))$
50	49	com13	$⊢ \{F (m), F (n)\} \in K \to ((m \in V \land n \in V) \to (φ \to \{m, n\} \in E))$
51	31 50	syl6bi	$⊢ (d = F (n) \land c = F (m)) \to (\{c, d\} \in K \to ((m \in V \land n \in V) \to (φ \to \{m, n\} \in E)))$
52	51	com14	$⊢ φ \to (\{c, d\} \in K \to ((m \in V \land n \in V) \to ((d = F (n) \land c = F (m)) \to \{m, n\} \in E)))$
53	52	imp	$⊢ (φ \land \{c, d\} \in K) \to ((m \in V \land n \in V) \to ((d = F (n) \land c = F (m)) \to \{m, n\} \in E))$
54	53	adantr	$⊢ ((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \to ((m \in V \land n \in V) \to ((d = F (n) \land c = F (m)) \to \{m, n\} \in E))$
55	54	imp31	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \to \{m, n\} \in E$
56		imaeq2	$⊢ e = \{m, n\} \to F [e] = F [\{m, n\}]$
57		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} W \to F Fn V$
58	7 57	syl	$⊢ φ \to F Fn V$
59	58	ad3antrrr	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \to F Fn V$
60		simprl	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \to m \in V$
61		simpr	$⊢ (m \in V \land n \in V) \to n \in V$
62	61	adantl	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \to n \in V$
63	59 60 62	3jca	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \to (F Fn V \land m \in V \land n \in V)$
64	63	adantr	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \to (F Fn V \land m \in V \land n \in V)$
65		fnimapr	$⊢ (F Fn V \land m \in V \land n \in V) \to F [\{m, n\}] = \{F (m), F (n)\}$
66	64 65	syl	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \to F [\{m, n\}] = \{F (m), F (n)\}$
67	56 66	sylan9eqr	$⊢ (((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \land e = \{m, n\}) \to F [e] = \{F (m), F (n)\}$
68	67	eqeq2d	$⊢ (((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \land e = \{m, n\}) \to (\{c, d\} = F [e] \leftrightarrow \{c, d\} = \{F (m), F (n)\})$
69	30	adantl	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \to \{c, d\} = \{F (m), F (n)\}$
70	55 68 69	rspcedvd	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \land (d = F (n) \land c = F (m))) \to \exists e \in E \{c, d\} = F [e]$
71	70	ex	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land (m \in V \land n \in V)) \to ((d = F (n) \land c = F (m)) \to \exists e \in E \{c, d\} = F [e])$
72	71	anassrs	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land m \in V) \land n \in V) \to ((d = F (n) \land c = F (m)) \to \exists e \in E \{c, d\} = F [e])$
73	72	expd	$⊢ ((((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land m \in V) \land n \in V) \to (d = F (n) \to (c = F (m) \to \exists e \in E \{c, d\} = F [e]))$
74	73	rexlimdva	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land m \in V) \to (\exists n \in V d = F (n) \to (c = F (m) \to \exists e \in E \{c, d\} = F [e]))$
75	74	com23	$⊢ (((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \land m \in V) \to (c = F (m) \to (\exists n \in V d = F (n) \to \exists e \in E \{c, d\} = F [e]))$
76	75	rexlimdva	$⊢ ((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \to (\exists m \in V c = F (m) \to (\exists n \in V d = F (n) \to \exists e \in E \{c, d\} = F [e]))$
77	76	impd	$⊢ ((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \to ((\exists m \in V c = F (m) \land \exists n \in V d = F (n)) \to \exists e \in E \{c, d\} = F [e])$
78	28 77	mpd	$⊢ ((φ \land \{c, d\} \in K) \land (c \in W \land d \in W)) \to \exists e \in E \{c, d\} = F [e]$
79	78	ex	$⊢ (φ \land \{c, d\} \in K) \to ((c \in W \land d \in W) \to \exists e \in E \{c, d\} = F [e])$
80	17 79	syl6bi	$⊢ y = \{c, d\} \to ((φ \land y \in K) \to ((c \in W \land d \in W) \to \exists e \in E \{c, d\} = F [e]))$
81	80	impd	$⊢ y = \{c, d\} \to (((φ \land y \in K) \land (c \in W \land d \in W)) \to \exists e \in E \{c, d\} = F [e])$
82	81	impcom	$⊢ (((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \to \exists e \in E \{c, d\} = F [e]$
83		simpr	$⊢ (((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \to y = \{c, d\}$
84	83	adantr	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to y = \{c, d\}$
85	9	ad4antr	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to F \in X$
86	1 2 3 4 5	isomuspgrlem2a	$⊢ F \in X \to \forall y \in E F [y] = G (y)$
87	85 86	syl	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to \forall y \in E F [y] = G (y)$
88		imaeq2	$⊢ y = e \to F [y] = F [e]$
89		fveq2	$⊢ y = e \to G (y) = G (e)$
90	88 89	eqeq12d	$⊢ y = e \to (F [y] = G (y) \leftrightarrow F [e] = G (e))$
91	90	rspcv	$⊢ e \in E \to (\forall y \in E F [y] = G (y) \to F [e] = G (e))$
92		eqcom	$⊢ G (e) = F [e] \leftrightarrow F [e] = G (e)$
93	91 92	syl6ibr	$⊢ e \in E \to (\forall y \in E F [y] = G (y) \to G (e) = F [e])$
94	93	adantl	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to (\forall y \in E F [y] = G (y) \to G (e) = F [e])$
95	87 94	mpd	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to G (e) = F [e]$
96	84 95	eqeq12d	$⊢ ((((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \land e \in E) \to (y = G (e) \leftrightarrow \{c, d\} = F [e])$
97	96	rexbidva	$⊢ (((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \to (\exists e \in E y = G (e) \leftrightarrow \exists e \in E \{c, d\} = F [e])$
98	82 97	mpbird	$⊢ (((φ \land y \in K) \land (c \in W \land d \in W)) \land y = \{c, d\}) \to \exists e \in E y = G (e)$
99	98	ex	$⊢ ((φ \land y \in K) \land (c \in W \land d \in W)) \to (y = \{c, d\} \to \exists e \in E y = G (e))$
100	99	rexlimdvva	$⊢ (φ \land y \in K) \to (\exists c \in W \exists d \in W y = \{c, d\} \to \exists e \in E y = G (e))$
101	15 100	mpd	$⊢ (φ \land y \in K) \to \exists e \in E y = G (e)$
102	101	ralrimiva	$⊢ φ \to \forall y \in K \exists e \in E y = G (e)$
103		dffo3	$⊢ G : E \underset{onto}{⟶} K \leftrightarrow (G : E ⟶ K \land \forall y \in K \exists e \in E y = G (e))$
104	11 102 103	sylanbrc	$⊢ φ \to G : E \underset{onto}{⟶} K$

Metamath Proof Explorer

Theorem isomuspgrlem2d

Proof