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 47452

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 47451	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)))
6	5	3expa 1115	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)))
7		simprl 769	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹:𝑉–1-1-onto→𝑊)
8		imaeq2 6065	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = {𝑥, 𝑦} → (𝐹 “ 𝑒) = (𝐹 “ {𝑥, 𝑦}))
9		eqidd 2727	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
10		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸)
11		f1ofun 6845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → Fun 𝐹)
12		zfpair2 5434	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥, 𝑦} ∈ V
13		funimaexg 6645	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ {𝑥, 𝑦} ∈ V) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
14	11, 12, 13	sylancl 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → (𝐹 “ {𝑥, 𝑦}) ∈ V)
15	14	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
16	8, 9, 10, 15	fvmptd4 7033	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
17	16	ex 411	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
18	17	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
19	18	ad2antlr 725	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
20	19	imp 405	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
21		f1of 6843	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
22	21	ad2antll 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷)
23		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
24		nnel 3046	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∅ ∉ 𝐷 ↔ ∅ ∈ 𝐷)
25		uspgruhgr 29120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph)
26		uhgredgn0 29064	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ UHGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
27	25, 26	sylan 578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
28		neldifsn 4801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅})
29	28	pm2.21i 119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) → ∅ ∉ 𝐷)
30	27, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∉ 𝐷)
31	30	expcom 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ (Edg‘𝐻) → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
32	31, 4	eleq2s 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
33	24, 32	sylbi 216	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
34	23, 33	pm2.61i 182	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ USPGraph → ∅ ∉ 𝐷)
35	34	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ∅ ∉ 𝐷)
36	22, 35	jca 510	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷))
37	36	adantr 479	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷))
38		feldmfvelcdm 7100	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸⟶𝐷 ∧ ∅ ∉ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
40	39	biimpa 475	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘{𝑥, 𝑦}) ∈ 𝐷)
41	20, 40	eqeltrrd 2827	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷)
42		imaeq2 6065	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹 “ {𝑥, 𝑦}) → (^◡𝐹 “ 𝑧) = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
43		imaeq2 6065	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑦 → (𝐹 “ 𝑒) = (𝐹 “ 𝑦))
44	43	cbvmptv 5266	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
45		f1oeq1 6831	. . . . . . . . . . . . . . . . 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 6065	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑥 → (𝐹 “ 𝑒) = (𝐹 “ 𝑥))
48	47	cbvmptv 5266	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥))
49		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → 𝐹:𝑉–1-1-onto→𝑊)
50	49	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐹:𝑉–1-1-onto→𝑊)
51		uspgruhgr 29120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
52		uhgredgss 29067	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))
53		difss2 4133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
54	51, 52, 53	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ∈ USPGraph → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
55	1	pweqi 4623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)
56	54, 3, 55	3sstr4g 4025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉)
57	56	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐸 ⊆ 𝒫 𝑉)
58	57	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐸 ⊆ 𝒫 𝑉)
59		f1ofo 6850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷)
60	44	rneqi 5943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦))
61		forn 6818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷 → ran (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)) = 𝐷)
62	60, 61	eqtrid 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
63	59, 62	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
64	63	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
65		uhgredgss 29067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐻 ∈ UHGraph → (Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}))
66		difss2 4133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}) → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
67	25, 65, 66	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐻 ∈ USPGraph → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
68	2	pweqi 4623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝒫 𝑊 = 𝒫 (Vtx‘𝐻)
69	67, 4, 68	3sstr4g 4025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊)
70	69	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐷 ⊆ 𝒫 𝑊)
71	70	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝐷 ⊆ 𝒫 𝑊)
72	64, 71	eqsstrd 4018	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ⊆ 𝒫 𝑊)
73	1	fvexi 6915	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑉 ∈ V
74	73	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → 𝑉 ∈ V)
75	48, 50, 58, 72, 74	mptcnfimad 8000	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ (𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
76	75	ex 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑦 ∈ 𝐸 ↦ (𝐹 “ 𝑦)):𝐸–1-1-onto→𝐷 → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧))))
77	46, 76	sylbid 239	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) → ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧))))
78	77	impr 453	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
79	78	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = (𝑧 ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) ↦ (^◡𝐹 “ 𝑧)))
80		f1ofo 6850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷)
81		forn 6818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷 → ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)) = 𝐷)
82	81	eqcomd 2732	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–onto→𝐷 → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
83	80, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
84	83	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
85	84	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝐷 = ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
86	85	eleq2d 2812	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))))
87	86	biimpa 475	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)))
88		dff1o2 6848	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑉–1-1-onto→𝑊 ↔ (𝐹 Fn 𝑉 ∧ Fun ^◡𝐹 ∧ ran 𝐹 = 𝑊))
89	88	simp2bi 1143	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → Fun ^◡𝐹)
90	89	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → Fun ^◡𝐹)
91	90	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → Fun ^◡𝐹)
92		funimaexg 6645	. . . . . . . . . . . . . 14 ⊢ ((Fun ^◡𝐹 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
93	91, 92	sylan 578	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
94	42, 79, 87, 93	fvmptd4 7033	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
95		simplrr 776	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)
96		f1ocnvdm 7299	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
97	95, 96	sylan 578	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡(𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
98	94, 97	eqeltrrd 2827	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
99		f1of1 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
100	99	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹:𝑉–1-1→𝑊)
101		prssi 4830	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑥, 𝑦} ⊆ 𝑉)
102		f1imacnv 6859	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ {𝑥, 𝑦} ⊆ 𝑉) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
103	100, 101, 102	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
104	103	eqcomd 2732	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → {𝑥, 𝑦} = (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})))
105	104	eleq1d 2811	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
106	105	adantr 479	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (^◡𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
107	98, 106	mpbird 256	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → {𝑥, 𝑦} ∈ 𝐸)
108	41, 107	impbida 799	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷))
109		f1ofn 6844	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉)
110	109	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → 𝐹 Fn 𝑉)
111	110	anim1i 613	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
112		3anass 1092	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
113	111, 112	sylibr 233	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))
114		fnimapr 6986	. . . . . . . . . . 11 ⊢ ((𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
115	113, 114	syl 17	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹‘𝑥), (𝐹‘𝑦)})
116	115	eleq1d 2811	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
117	108, 116	bitrd 278	. . . . . . . 8 ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
118	117	ralrimivva 3191	. . . . . . 7 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))
119	7, 118	jca 510	. . . . . 6 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))
120	119	ex 411	. . . . 5 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
121	120	adantr 479	. . . 4 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → ((𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
122	6, 121	sylbid 239	. . 3 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))
123	122	syldbl2 839	. 2 ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))
124	123	ex 411	1 ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ∉ wnel 3036 ∀wral 3051 Vcvv 3462 ∖ cdif 3944 ⊆ wss 3947 ∅c0 4325 𝒫 cpw 4607 {csn 4633 {cpr 4635 ↦ cmpt 5236 ^◡ccnv 5681 ran crn 5683 “ cima 5685 Fun wfun 6548 Fn wfn 6549 ⟶wf 6550 –1-1→wf1 6551 –onto→wfo 6552 –1-1-onto→wf1o 6553 ‘cfv 6554 (class class class)co 7424 Vtxcvtx 28932 Edgcedg 28983 UHGraphcuhgr 28992 USPGraphcuspgr 29084 GraphIso cgrim 47440

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-map 8857 df-edg 28984 df-uhgr 28994 df-upgr 29018 df-uspgr 29086 df-grim 47443

This theorem is referenced by: isuspgrim 47454

W3C validator