grimuhgr

Description: If there is a graph isomorphism between a hypergraph and a class with an edge function, the class is also a hypergraph. (Contributed by AV, 2-May-2025)

		Ref	Expression
	Assertion	grimuhgr	$⊢ (S \in UHGraph \land F \in (S GraphIso T) \land Fun iEdg (T)) \to T \in UHGraph$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (S) = Vtx (S)$
2		eqid	$⊢ Vtx (T) = Vtx (T)$
3		eqid	$⊢ iEdg (S) = iEdg (S)$
4		eqid	$⊢ iEdg (T) = iEdg (T)$
5	1 2 3 4	grimprop	$⊢ F \in (S GraphIso T) \to (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))$
6		fdmrn	$⊢ Fun iEdg (T) \leftrightarrow iEdg (T) : dom iEdg (T) ⟶ ran iEdg (T)$
7	6	biimpi	$⊢ Fun iEdg (T) \to iEdg (T) : dom iEdg (T) ⟶ ran iEdg (T)$
8	7	3ad2ant3	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \to iEdg (T) : dom iEdg (T) ⟶ ran iEdg (T)$
9	8	adantr	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to iEdg (T) : dom iEdg (T) ⟶ ran iEdg (T)$
10		funfn	$⊢ Fun iEdg (T) \leftrightarrow iEdg (T) Fn dom iEdg (T)$
11	10	biimpi	$⊢ Fun iEdg (T) \to iEdg (T) Fn dom iEdg (T)$
12	11	3ad2ant3	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \to iEdg (T) Fn dom iEdg (T)$
13		f1ofo	$⊢ j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T)$
14	13	3ad2ant2	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T)$
15	14	3ad2ant1	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T)$
16		foelcdmi	$⊢ (j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T) \land x \in dom iEdg (T)) \to \exists y \in dom iEdg (S) j (y) = x$
17	15 16	sylan	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land x \in dom iEdg (T)) \to \exists y \in dom iEdg (S) j (y) = x$
18	17	ex	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (x \in dom iEdg (T) \to \exists y \in dom iEdg (S) j (y) = x)$
19		2fveq3	$⊢ i = y \to iEdg (T) (j (i)) = iEdg (T) (j (y))$
20		fveq2	$⊢ i = y \to iEdg (S) (i) = iEdg (S) (y)$
21	20	imaeq2d	$⊢ i = y \to F [iEdg (S) (i)] = F [iEdg (S) (y)]$
22	19 21	eqeq12d	$⊢ i = y \to (iEdg (T) (j (i)) = F [iEdg (S) (i)] \leftrightarrow iEdg (T) (j (y)) = F [iEdg (S) (y)])$
23	22	rspcv	$⊢ y \in dom iEdg (S) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to iEdg (T) (j (y)) = F [iEdg (S) (y)])$
24	23	adantl	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to iEdg (T) (j (y)) = F [iEdg (S) (y)])$
25		f1ofun	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to Fun F$
26	25	3ad2ant1	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to Fun F$
27	26	adantr	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \to Fun F$
28		fvex	$⊢ iEdg (S) (y) \in V$
29	28	a1i	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to iEdg (S) (y) \in V$
30		funimaexg	$⊢ (Fun F \land iEdg (S) (y) \in V) \to F [iEdg (S) (y)] \in V$
31	27 29 30	syl2an2r	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to F [iEdg (S) (y)] \in V$
32		f1of	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to F : Vtx (S) ⟶ Vtx (T)$
33	32	fimassd	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to F [iEdg (S) (y)] \subseteq Vtx (T)$
34	33	3ad2ant1	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to F [iEdg (S) (y)] \subseteq Vtx (T)$
35	34	adantr	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \to F [iEdg (S) (y)] \subseteq Vtx (T)$
36	35	adantr	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to F [iEdg (S) (y)] \subseteq Vtx (T)$
37	31 36	elpwd	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to F [iEdg (S) (y)] \in 𝒫 Vtx (T)$
38		f1odm	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to dom F = Vtx (S)$
39	38	adantr	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to dom F = Vtx (S)$
40	39	adantr	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land y \in dom iEdg (S)) \to dom F = Vtx (S)$
41	40	ineq1d	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land y \in dom iEdg (S)) \to dom F \cap iEdg (S) (y) = Vtx (S) \cap iEdg (S) (y)$
42		ffvelcdm	$⊢ (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \land y \in dom iEdg (S)) \to iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\})$
43	42	ex	$⊢ iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to (y \in dom iEdg (S) \to iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\}))$
44	43	adantl	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (y \in dom iEdg (S) \to iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\}))$
45		eldifsn	$⊢ iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\}) \leftrightarrow (iEdg (S) (y) \in 𝒫 Vtx (S) \land iEdg (S) (y) \neq \emptyset)$
46	28	elpw	$⊢ iEdg (S) (y) \in 𝒫 Vtx (S) \leftrightarrow iEdg (S) (y) \subseteq Vtx (S)$
47	45 46	bianbi	$⊢ iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\}) \leftrightarrow (iEdg (S) (y) \subseteq Vtx (S) \land iEdg (S) (y) \neq \emptyset)$
48		sseqin2	$⊢ iEdg (S) (y) \subseteq Vtx (S) \leftrightarrow Vtx (S) \cap iEdg (S) (y) = iEdg (S) (y)$
49	48	biimpi	$⊢ iEdg (S) (y) \subseteq Vtx (S) \to Vtx (S) \cap iEdg (S) (y) = iEdg (S) (y)$
50	49	adantr	$⊢ (iEdg (S) (y) \subseteq Vtx (S) \land iEdg (S) (y) \neq \emptyset) \to Vtx (S) \cap iEdg (S) (y) = iEdg (S) (y)$
51		simpr	$⊢ (iEdg (S) (y) \subseteq Vtx (S) \land iEdg (S) (y) \neq \emptyset) \to iEdg (S) (y) \neq \emptyset$
52	50 51	eqnetrd	$⊢ (iEdg (S) (y) \subseteq Vtx (S) \land iEdg (S) (y) \neq \emptyset) \to Vtx (S) \cap iEdg (S) (y) \neq \emptyset$
53	52	a1i	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to ((iEdg (S) (y) \subseteq Vtx (S) \land iEdg (S) (y) \neq \emptyset) \to Vtx (S) \cap iEdg (S) (y) \neq \emptyset)$
54	47 53	biimtrid	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (iEdg (S) (y) \in (𝒫 Vtx (S) ∖ \{\emptyset\}) \to Vtx (S) \cap iEdg (S) (y) \neq \emptyset)$
55	44 54	syld	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (y \in dom iEdg (S) \to Vtx (S) \cap iEdg (S) (y) \neq \emptyset)$
56	55	imp	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land y \in dom iEdg (S)) \to Vtx (S) \cap iEdg (S) (y) \neq \emptyset$
57	41 56	eqnetrd	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land y \in dom iEdg (S)) \to dom F \cap iEdg (S) (y) \neq \emptyset$
58	57	ex	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (y \in dom iEdg (S) \to dom F \cap iEdg (S) (y) \neq \emptyset)$
59	58	3adant2	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (y \in dom iEdg (S) \to dom F \cap iEdg (S) (y) \neq \emptyset)$
60	59	adantr	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \to (y \in dom iEdg (S) \to dom F \cap iEdg (S) (y) \neq \emptyset)$
61	60	imp	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to dom F \cap iEdg (S) (y) \neq \emptyset$
62	61	imadisjlnd	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to F [iEdg (S) (y)] \neq \emptyset$
63		eldifsn	$⊢ F [iEdg (S) (y)] \in (𝒫 Vtx (T) ∖ \{\emptyset\}) \leftrightarrow (F [iEdg (S) (y)] \in 𝒫 Vtx (T) \land F [iEdg (S) (y)] \neq \emptyset)$
64	37 62 63	sylanbrc	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to F [iEdg (S) (y)] \in (𝒫 Vtx (T) ∖ \{\emptyset\})$
65	64	adantr	$⊢ ((((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \to F [iEdg (S) (y)] \in (𝒫 Vtx (T) ∖ \{\emptyset\})$
66		eleq1	$⊢ iEdg (T) (j (y)) = F [iEdg (S) (y)] \to (iEdg (T) (j (y)) \in (𝒫 Vtx (T) ∖ \{\emptyset\}) \leftrightarrow F [iEdg (S) (y)] \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
67	66	adantl	$⊢ ((((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \to (iEdg (T) (j (y)) \in (𝒫 Vtx (T) ∖ \{\emptyset\}) \leftrightarrow F [iEdg (S) (y)] \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
68	65 67	mpbird	$⊢ ((((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \to iEdg (T) (j (y)) \in (𝒫 Vtx (T) ∖ \{\emptyset\})$
69		fveq2	$⊢ j (y) = x \to iEdg (T) (j (y)) = iEdg (T) (x)$
70	69	eleq1d	$⊢ j (y) = x \to (iEdg (T) (j (y)) \in (𝒫 Vtx (T) ∖ \{\emptyset\}) \leftrightarrow iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
71	68 70	syl5ibcom	$⊢ ((((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
72	71	ex	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to (iEdg (T) (j (y)) = F [iEdg (S) (y)] \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))$
73	24 72	syld	$⊢ (((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \land y \in dom iEdg (S)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))$
74	73	ex	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \to (y \in dom iEdg (S) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))))$
75	74	com23	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (y \in dom iEdg (S) \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))))$
76	75	ex	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (Fun iEdg (T) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (y \in dom iEdg (S) \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))))$
77	76	3imp	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (y \in dom iEdg (S) \to (j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))$
78	77	rexlimdv	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (\exists y \in dom iEdg (S) j (y) = x \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
79	18 78	syld	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (x \in dom iEdg (T) \to iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
80	79	ralrimiv	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \land Fun iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})$
81	80	3exp	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to (Fun iEdg (T) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))$
82	81	3exp	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to (Fun iEdg (T) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))))$
83	82	com35	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})))))$
84	83	impd	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to ((j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))))$
85	84	3imp	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\}))$
86	85	imp	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})$
87		fnfvrnss	$⊢ (iEdg (T) Fn dom iEdg (T) \land \forall x \in dom iEdg (T) iEdg (T) (x) \in (𝒫 Vtx (T) ∖ \{\emptyset\})) \to ran iEdg (T) \subseteq 𝒫 Vtx (T) ∖ \{\emptyset\}$
88	12 86 87	syl2an2r	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to ran iEdg (T) \subseteq 𝒫 Vtx (T) ∖ \{\emptyset\}$
89	9 88	fssd	$⊢ ((F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \land iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}) \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}$
90	89	ex	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \land Fun iEdg (T)) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})$
91	90	3exp	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to ((j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})))$
92	91	exlimdv	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to (\exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})))$
93	92	imp	$⊢ (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}))$
94	5 93	syl	$⊢ F \in (S GraphIso T) \to (Fun iEdg (T) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}))$
95	94	impcom	$⊢ (Fun iEdg (T) \land F \in (S GraphIso T)) \to (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})$
96		grimdmrel	$⊢ Rel dom GraphIso$
97	96	ovrcl	$⊢ F \in (S GraphIso T) \to (S \in V \land T \in V)$
98	1 3	isuhgr	$⊢ S \in V \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
99	98	adantr	$⊢ (S \in V \land T \in V) \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
100	2 4	isuhgr	$⊢ T \in V \to (T \in UHGraph \leftrightarrow iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})$
101	100	adantl	$⊢ (S \in V \land T \in V) \to (T \in UHGraph \leftrightarrow iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\})$
102	99 101	imbi12d	$⊢ (S \in V \land T \in V) \to ((S \in UHGraph \to T \in UHGraph) \leftrightarrow (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}))$
103	97 102	syl	$⊢ F \in (S GraphIso T) \to ((S \in UHGraph \to T \in UHGraph) \leftrightarrow (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}))$
104	103	adantl	$⊢ (Fun iEdg (T) \land F \in (S GraphIso T)) \to ((S \in UHGraph \to T \in UHGraph) \leftrightarrow (iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \to iEdg (T) : dom iEdg (T) ⟶ 𝒫 Vtx (T) ∖ \{\emptyset\}))$
105	95 104	mpbird	$⊢ (Fun iEdg (T) \land F \in (S GraphIso T)) \to (S \in UHGraph \to T \in UHGraph)$
106	105	ex	$⊢ Fun iEdg (T) \to (F \in (S GraphIso T) \to (S \in UHGraph \to T \in UHGraph))$
107	106	3imp31	$⊢ (S \in UHGraph \land F \in (S GraphIso T) \land Fun iEdg (T)) \to T \in UHGraph$

Metamath Proof Explorer

Theorem grimuhgr

Proof