uspgrimprop - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > uspgrimprop		Structured version Visualization version GIF version

Theorem uspgrimprop 47878

Description: An isomorphism of simple pseudographs is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025.)

**Hypotheses**
Ref	Expression
isusgrim.v	⊢ 𝑉 = (Vtx‘𝐺)
isusgrim.w	⊢ 𝑊 = (Vtx‘𝐻)
isusgrim.e	⊢ 𝐸 = (Edg‘𝐺)
isusgrim.d	⊢ 𝐷 = (Edg‘𝐻)

**Assertion**
Ref	Expression
uspgrimprop	⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))

Distinct variable groups: 𝑥,𝐸 𝑥,𝐹 𝑥,𝐷,𝑦 𝑦,𝐸 𝑦,𝐹 𝑥,𝐺,𝑦 𝑥,𝐻,𝑦 𝑥,𝑉,𝑦 𝑥,𝑊,𝑦

Proof of Theorem uspgrimprop Dummy variables 𝑒 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isusgrim.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2		isusgrim.w	. . . . . 6 ⊢ 𝑊 = (Vtx‘𝐻)
3		isusgrim.e	. . . . . 6 ⊢ 𝐸 = (Edg‘𝐺)
4		isusgrim.d	. . . . . 6 ⊢ 𝐷 = (Edg‘𝐻)
5	1, 2, 3, 4	isuspgrim0 47877	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)))
6	5	3expa 1118	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)))
7		simprl 770	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹:𝑉–1-1-onto→𝑊)
8		imaeq2 6073	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = {𝑥, 𝑦} → (𝐹 “ 𝑒) = (𝐹 “ {𝑥, 𝑦}))
9		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
10		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸)
11		f1ofun 6849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → Fun 𝐹)
12		zfpair2 5432	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥, 𝑦} ∈ V
13		funimaexg 6652	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ {𝑥, 𝑦} ∈ V) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
14	11, 12, 13	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (𝐹 “ {𝑥, 𝑦}) ∈ V)
15	14	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
16	8, 9, 10, 15	fvmptd4 7039	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
17	16	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
18	17	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
19	18	ad2antlr 727	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
20	19	imp 406	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
21		f1of 6847	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
22	21	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
23		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
24		nnel 3055	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∅ ∉ 𝐷 ↔ ∅ ∈ 𝐷)
25		uspgruhgr 29202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph)
26		uhgredgn0 29146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ UHGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
27	25, 26	sylan 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
28		neldifsn 4791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅})
29	28	pm2.21i 119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) → ∅ ∉ 𝐷)
30	27, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∉ 𝐷)
31	30	expcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ (Edg‘𝐻) → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
32	31, 4	eleq2s 2858	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
33	24, 32	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
34	23, 33	pm2.61i 182	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ USPGraph → ∅ ∉ 𝐷)
35	34	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ∅ ∉ 𝐷)
36	22, 35	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷))
37	36	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷))
38		feldmfvelcdm 7105	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
40	39	biimpa 476	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷)
41	20, 40	eqeltrrd 2841	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷)
42		imaeq2 6073	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹 “ {𝑥, 𝑦}) → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
43		imaeq2 6073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑦 → (𝐹 “ 𝑒) = (𝐹 “ 𝑦))
44	43	cbvmptv 5254	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
45		f1oeq1 6835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 ↔ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷))
46	44, 45	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 ↔ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷))
47		imaeq2 6073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑥 → (𝐹 “ 𝑒) = (𝐹 “ 𝑥))
48	47	cbvmptv 5254	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
49		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → 𝐹:𝑉–1-1-onto→𝑊)
50	49	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐹:𝑉–1-1-onto→𝑊)
51		uspgruhgr 29202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
52		uhgredgss 29149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))
53		difss2 4137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
54	51, 52, 53	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ∈ USPGraph → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
55	1	pweqi 4615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)
56	54, 3, 55	3sstr4g 4036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉)
57	56	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐸 ⊆ 𝒫 𝑉)
58	57	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐸 ⊆ 𝒫 𝑉)
59		f1ofo 6854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷)
60	44	rneqi 5947	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
61		forn 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷 → ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)) = 𝐷)
62	60, 61	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
63	59, 62	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
64	63	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
65		uhgredgss 29149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐻 ∈ UHGraph → (Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}))
66		difss2 4137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}) → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
67	25, 65, 66	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
68	2	pweqi 4615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝒫 𝑊 = 𝒫 (Vtx‘𝐻)
69	67, 4, 68	3sstr4g 4036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊)
70	69	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐷 ⊆ 𝒫 𝑊)
71	70	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐷 ⊆ 𝒫 𝑊)
72	64, 71	eqsstrd 4017	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ⊆ 𝒫 𝑊)
73	1	fvexi 6919	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 ∈ V
74	73	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝑉 ∈ V)
75	48, 50, 58, 72, 74	mptcnfimad 8012	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
76	75	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧))))
77	46, 76	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧))))
78	77	impr 454	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
79	78	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
80		f1ofo 6854	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷)
81		forn 6822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
82	81	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷 → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
83	80, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
84	83	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
85	84	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
86	85	eleq2d 2826	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))))
87	86	biimpa 476	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
88		dff1o2 6852	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→𝑊 ↔ (𝐹 Fn 𝑉 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝑊))
89	88	simp2bi 1146	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → Fun ^◡𝐹)
90	89	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → Fun ^◡𝐹)
91	90	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → Fun ^◡𝐹)
92		funimaexg 6652	. . . . . . . . . . . . . 14 ⊢ ((Fun ^◡𝐹 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
93	91, 92	sylan 580	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
94	42, 79, 87, 93	fvmptd4 7039	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
95		simplrr 777	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
96		f1ocnvdm 7306	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
97	95, 96	sylan 580	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
98	94, 97	eqeltrrd 2841	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
99		f1of1 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
100	99	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹:𝑉–1-1→𝑊)
101		prssi 4820	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑥, 𝑦} ⊆ 𝑉)
102		f1imacnv 6863	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ {𝑥, 𝑦} ⊆ 𝑉) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
103	100, 101, 102	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
104	103	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → {𝑥, 𝑦} = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
105	104	eleq1d 2825	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
106	105	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
107	98, 106	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → {𝑥, 𝑦} ∈ 𝐸)
108	41, 107	impbida 800	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷))
109		f1ofn 6848	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
110	109	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹 Fn 𝑉)
111	110	anim1i 615	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
112		3anass 1094	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
113	111, 112	sylibr 234	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))
114		fnimapr 6991	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
115	113, 114	syl 17	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
116	115	eleq1d 2825	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
117	108, 116	bitrd 279	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
118	117	ralrimivva 3201	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
119	7, 118	jca 511	. . . . . 6 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))
120	119	ex 412	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
121	120	adantr 480	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
122	6, 121	sylbid 240	. . 3 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
123	122	syldbl2 841	. 2 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))
124	123	ex 412	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ∉ wnel 3045 ∀wral 3060 Vcvv 3479 ∖ cdif 3947 ⊆ wss 3950 ∅c0 4332 𝒫 cpw 4599 {csn 4625 {cpr 4627 ↦ cmpt 5224 ^◡ccnv 5683 ran crn 5685 “ cima 5687 Fun wfun 6554 Fn wfn 6555 ⟶wf 6556 –1-1→wf1 6557 –onto→wfo 6558 –1-1-onto→wf1o 6559 ‘cfv 6560 (class class class)co 7432 Vtxcvtx 29014 Edgcedg 29065 UHGraphcuhgr 29074 USPGraphcuspgr 29166 GraphIso cgrim 47866

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-ov 7435 df-oprab 7436 df-mpo 7437 df-map 8869 df-edg 29066 df-uhgr 29076 df-upgr 29100 df-uspgr 29168 df-grim 47869

This theorem is referenced by: isuspgrim 47880

W3C validator