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 47757

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 47756	. . . . 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 6085	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = {𝑥, 𝑦} → (𝐹 “ 𝑒) = (𝐹 “ {𝑥, 𝑦}))
9		eqidd 2741	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
10		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸)
11		f1ofun 6864	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → Fun 𝐹)
12		zfpair2 5448	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥, 𝑦} ∈ V
13		funimaexg 6664	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ {𝑥, 𝑦} ∈ V) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
14	11, 12, 13	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (𝐹 “ {𝑥, 𝑦}) ∈ V)
15	14	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
16	8, 9, 10, 15	fvmptd4 7053	. . . . . . . . . . . . . . 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 726	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
20	19	imp 406	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
21		f1of 6862	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
22	21	ad2antll 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
23		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
24		nnel 3062	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∅ ∉ 𝐷 ↔ ∅ ∈ 𝐷)
25		uspgruhgr 29219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph)
26		uhgredgn0 29163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ UHGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
27	25, 26	sylan 579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
28		neldifsn 4817	. . . . . . . . . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
33	24, 32	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
34	23, 33	pm2.61i 182	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ USPGraph → ∅ ∉ 𝐷)
35	34	ad2antlr 726	. . . . . . . . . . . . . . 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 7120	. . . . . . . . . . . . 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 2845	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷)
42		imaeq2 6085	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹 “ {𝑥, 𝑦}) → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
43		imaeq2 6085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑦 → (𝐹 “ 𝑒) = (𝐹 “ 𝑦))
44	43	cbvmptv 5279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
45		f1oeq1 6850	. . . . . . . . . . . . . . . . 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 6085	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑥 → (𝐹 “ 𝑒) = (𝐹 “ 𝑥))
48	47	cbvmptv 5279	. . . . . . . . . . . . . . . . . 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 29219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
52		uhgredgss 29166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))
53		difss2 4161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
54	51, 52, 53	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ∈ USPGraph → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
55	1	pweqi 4638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)
56	54, 3, 55	3sstr4g 4054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉)
57	56	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐸 ⊆ 𝒫 𝑉)
58	57	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐸 ⊆ 𝒫 𝑉)
59		f1ofo 6869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷)
60	44	rneqi 5962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
61		forn 6837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷 → ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)) = 𝐷)
62	60, 61	eqtrid 2792	. . . . . . . . . . . . . . . . . . . . 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 29166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐻 ∈ UHGraph → (Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}))
66		difss2 4161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}) → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
67	25, 65, 66	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
68	2	pweqi 4638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝒫 𝑊 = 𝒫 (Vtx‘𝐻)
69	67, 4, 68	3sstr4g 4054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊)
70	69	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐷 ⊆ 𝒫 𝑊)
71	70	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐷 ⊆ 𝒫 𝑊)
72	64, 71	eqsstrd 4047	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ⊆ 𝒫 𝑊)
73	1	fvexi 6934	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 ∈ V
74	73	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝑉 ∈ V)
75	48, 50, 58, 72, 74	mptcnfimad 8027	. . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
80		f1ofo 6869	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷)
81		forn 6837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
82	81	eqcomd 2746	. . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
86	85	eleq2d 2830	. . . . . . . . . . . . . 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 6867	. . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → Fun ^◡𝐹)
92		funimaexg 6664	. . . . . . . . . . . . . 14 ⊢ ((Fun ^◡𝐹 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
93	91, 92	sylan 579	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
94	42, 79, 87, 93	fvmptd4 7053	. . . . . . . . . . . 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 7321	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
97	95, 96	sylan 579	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
98	94, 97	eqeltrrd 2845	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
99		f1of1 6861	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
100	99	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹:𝑉–1-1→𝑊)
101		prssi 4846	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑥, 𝑦} ⊆ 𝑉)
102		f1imacnv 6878	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ {𝑥, 𝑦} ⊆ 𝑉) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
103	100, 101, 102	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
104	103	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → {𝑥, 𝑦} = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
105	104	eleq1d 2829	. . . . . . . . . . . 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 6863	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
110	109	ad2antrl 727	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹 Fn 𝑉)
111	110	anim1i 614	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
112		3anass 1095	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
113	111, 112	sylibr 234	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))
114		fnimapr 7005	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
115	113, 114	syl 17	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
116	115	eleq1d 2829	. . . . . . . . 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 3208	. . . . . . 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 840	. 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 1087 = wceq 1537 ∈ wcel 2108 ∉ wnel 3052 ∀wral 3067 Vcvv 3488 ∖ cdif 3973 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 {csn 4648 {cpr 4650 ↦ cmpt 5249 ^◡ccnv 5699 ran crn 5701 “ cima 5703 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –1-1→wf1 6570 –onto→wfo 6571 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 Vtxcvtx 29031 Edgcedg 29082 UHGraphcuhgr 29091 USPGraphcuspgr 29183 GraphIso cgrim 47745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-oprab 7452 df-mpo 7453 df-map 8886 df-edg 29083 df-uhgr 29093 df-upgr 29117 df-uspgr 29185 df-grim 47748

This theorem is referenced by: isuspgrim 47759

W3C validator