Users' Mathboxes 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.
StepHypRef Expression
1 isusgrim.v . . . . . 6 𝑉 = (Vtx‘𝐺)
2 isusgrim.w . . . . . 6 𝑊 = (Vtx‘𝐻)
3 isusgrim.e . . . . . 6 𝐸 = (Edg‘𝐺)
4 isusgrim.d . . . . . 6 𝐷 = (Edg‘𝐻)
51, 2, 3, 4isuspgrim0 47877 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
653expa 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)
1411, 12, 13sylancl 586 . . . . . . . . . . . . . . . . 17 (𝐹:𝑉1-1-onto𝑊 → (𝐹 “ {𝑥, 𝑦}) ∈ V)
1514adantr 480 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉1-1-onto𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
168, 9, 10, 15fvmptd4 7039 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1-onto𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
1716ex 412 . . . . . . . . . . . . . 14 (𝐹:𝑉1-1-onto𝑊 → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
1817adantr 480 . . . . . . . . . . . . 13 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
1918ad2antlr 727 . . . . . . . . . . . 12 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦})))
2019imp 406 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) = (𝐹 “ {𝑥, 𝑦}))
21 f1of 6847 . . . . . . . . . . . . . . . 16 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 → (𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷)
2221ad2antll 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‘𝐻) ∖ {∅}))
2725, 26sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
28 neldifsn 4791 . . . . . . . . . . . . . . . . . . . . . 22 ¬ ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅})
2928pm2.21i 119 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) → ∅ ∉ 𝐷)
3027, 29syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∉ 𝐷)
3130expcom 413 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ (Edg‘𝐻) → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
3231, 4eleq2s 2858 . . . . . . . . . . . . . . . . . 18 (∅ ∈ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
3324, 32sylbi 217 . . . . . . . . . . . . . . . . 17 (¬ ∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
3423, 33pm2.61i 182 . . . . . . . . . . . . . . . 16 (𝐻 ∈ USPGraph → ∅ ∉ 𝐷)
3534ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → ∅ ∉ 𝐷)
3622, 35jca 511 . . . . . . . . . . . . . 14 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷 ∧ ∅ ∉ 𝐷))
3736adantr 480 . . . . . . . . . . . . 13 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷 ∧ ∅ ∉ 𝐷))
38 feldmfvelcdm 7105 . . . . . . . . . . . . 13 (((𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷 ∧ ∅ ∉ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
3937, 38syl 17 . . . . . . . . . . . 12 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) ∈ 𝐷))
4039biimpa 476 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑒𝐸 ↦ (𝐹𝑒))‘{𝑥, 𝑦}) ∈ 𝐷)
4120, 40eqeltrrd 2841 . . . . . . . . . 10 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷)
42 imaeq2 6073 . . . . . . . . . . . . 13 (𝑧 = (𝐹 “ {𝑥, 𝑦}) → (𝐹𝑧) = (𝐹 “ (𝐹 “ {𝑥, 𝑦})))
43 imaeq2 6073 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑦 → (𝐹𝑒) = (𝐹𝑦))
4443cbvmptv 5254 . . . . . . . . . . . . . . . . 17 (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑦𝐸 ↦ (𝐹𝑦))
45 f1oeq1 6835 . . . . . . . . . . . . . . . . 17 ((𝑒𝐸 ↦ (𝐹𝑒)) = (𝑦𝐸 ↦ (𝐹𝑦)) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 ↔ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷))
4644, 45mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 ↔ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷))
47 imaeq2 6073 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑥 → (𝐹𝑒) = (𝐹𝑥))
4847cbvmptv 5254 . . . . . . . . . . . . . . . . . 18 (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑥𝐸 ↦ (𝐹𝑥))
49 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) → 𝐹:𝑉1-1-onto𝑊)
5049adantr 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‘𝐺))
5451, 52, 533syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ∈ USPGraph → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
551pweqi 4615 . . . . . . . . . . . . . . . . . . . . 21 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)
5654, 3, 553sstr4g 4036 . . . . . . . . . . . . . . . . . . . 20 (𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉)
5756adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐸 ⊆ 𝒫 𝑉)
5857ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝐸 ⊆ 𝒫 𝑉)
59 f1ofo 6854 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷 → (𝑦𝐸 ↦ (𝐹𝑦)):𝐸onto𝐷)
6044rneqi 5947 . . . . . . . . . . . . . . . . . . . . . 22 ran (𝑒𝐸 ↦ (𝐹𝑒)) = ran (𝑦𝐸 ↦ (𝐹𝑦))
61 forn 6822 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸onto𝐷 → ran (𝑦𝐸 ↦ (𝐹𝑦)) = 𝐷)
6260, 61eqtrid 2788 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸onto𝐷 → ran (𝑒𝐸 ↦ (𝐹𝑒)) = 𝐷)
6359, 62syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷 → ran (𝑒𝐸 ↦ (𝐹𝑒)) = 𝐷)
6463adantl 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‘𝐻))
6725, 65, 663syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻 ∈ USPGraph → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
682pweqi 4615 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 𝑊 = 𝒫 (Vtx‘𝐻)
6967, 4, 683sstr4g 4036 . . . . . . . . . . . . . . . . . . . . 21 (𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊)
7069adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐷 ⊆ 𝒫 𝑊)
7170ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝐷 ⊆ 𝒫 𝑊)
7264, 71eqsstrd 4017 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → ran (𝑒𝐸 ↦ (𝐹𝑒)) ⊆ 𝒫 𝑊)
731fvexi 6919 . . . . . . . . . . . . . . . . . . 19 𝑉 ∈ V
7473a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝑉 ∈ V)
7548, 50, 58, 72, 74mptcnfimad 8012 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑧 ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)) ↦ (𝐹𝑧)))
7675ex 412 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷(𝑒𝐸 ↦ (𝐹𝑒)) = (𝑧 ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)) ↦ (𝐹𝑧))))
7746, 76sylbid 240 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷(𝑒𝐸 ↦ (𝐹𝑒)) = (𝑧 ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)) ↦ (𝐹𝑧))))
7877impr 454 . . . . . . . . . . . . . 14 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑧 ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)) ↦ (𝐹𝑧)))
7978ad2antrr 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 (𝑒𝐸 ↦ (𝐹𝑒)) = 𝐷)
8281eqcomd 2742 . . . . . . . . . . . . . . . . . 18 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸onto𝐷𝐷 = ran (𝑒𝐸 ↦ (𝐹𝑒)))
8380, 82syl 17 . . . . . . . . . . . . . . . . 17 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷𝐷 = ran (𝑒𝐸 ↦ (𝐹𝑒)))
8483adantl 481 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷) → 𝐷 = ran (𝑒𝐸 ↦ (𝐹𝑒)))
8584ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → 𝐷 = ran (𝑒𝐸 ↦ (𝐹𝑒)))
8685eleq2d 2826 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒𝐸 ↦ (𝐹𝑒))))
8786biimpa 476 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)))
88 dff1o2 6852 . . . . . . . . . . . . . . . . 17 (𝐹:𝑉1-1-onto𝑊 ↔ (𝐹 Fn 𝑉 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝑊))
8988simp2bi 1146 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝑊 → Fun 𝐹)
9089adantr 480 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷) → Fun 𝐹)
9190ad2antlr 727 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → Fun 𝐹)
92 funimaexg 6652 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
9391, 92sylan 580 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
9442, 79, 87, 93fvmptd4 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𝐷 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ((𝑒𝐸 ↦ (𝐹𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
9795, 96sylan 580 . . . . . . . . . . . 12 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ((𝑒𝐸 ↦ (𝐹𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
9894, 97eqeltrrd 2841 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
99 f1of1 6846 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝑊𝐹:𝑉1-1𝑊)
10099ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → 𝐹:𝑉1-1𝑊)
101 prssi 4820 . . . . . . . . . . . . . . 15 ((𝑥𝑉𝑦𝑉) → {𝑥, 𝑦} ⊆ 𝑉)
102 f1imacnv 6863 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝑊 ∧ {𝑥, 𝑦} ⊆ 𝑉) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
103100, 101, 102syl2an 596 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
104103eqcomd 2742 . . . . . . . . . . . . 13 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → {𝑥, 𝑦} = (𝐹 “ (𝐹 “ {𝑥, 𝑦})))
105104eleq1d 2825 . . . . . . . . . . . 12 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
106105adantr 480 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸))
10798, 106mpbird 257 . . . . . . . . . 10 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → {𝑥, 𝑦} ∈ 𝐸)
10841, 107impbida 800 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷))
109 f1ofn 6848 . . . . . . . . . . . . . 14 (𝐹:𝑉1-1-onto𝑊𝐹 Fn 𝑉)
110109ad2antrl 728 . . . . . . . . . . . . 13 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → 𝐹 Fn 𝑉)
111110anim1i 615 . . . . . . . . . . . 12 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 Fn 𝑉 ∧ (𝑥𝑉𝑦𝑉)))
112 3anass 1094 . . . . . . . . . . . 12 ((𝐹 Fn 𝑉𝑥𝑉𝑦𝑉) ↔ (𝐹 Fn 𝑉 ∧ (𝑥𝑉𝑦𝑉)))
113111, 112sylibr 234 . . . . . . . . . . 11 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 Fn 𝑉𝑥𝑉𝑦𝑉))
114 fnimapr 6991 . . . . . . . . . . 11 ((𝐹 Fn 𝑉𝑥𝑉𝑦𝑉) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹𝑥), (𝐹𝑦)})
115113, 114syl 17 . . . . . . . . . 10 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹𝑥), (𝐹𝑦)})
116115eleq1d 2825 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))
117108, 116bitrd 279 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))
118117ralrimivva 3201 . . . . . . 7 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))
1197, 118jca 511 . . . . . 6 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → (𝐹:𝑉1-1-onto𝑊 ∧ ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷)))
120119ex 412 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷) → (𝐹:𝑉1-1-onto𝑊 ∧ ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))))
121120adantr 480 . . . 4 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → ((𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷) → (𝐹:𝑉1-1-onto𝑊 ∧ ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))))
1226, 121sylbid 240 . . 3 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉1-1-onto𝑊 ∧ ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))))
123122syldbl2 841 . 2 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹:𝑉1-1-onto𝑊 ∧ ∀𝑥𝑉𝑦𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷)))
124123ex 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-1wf1 6557  ontowfo 6558  1-1-ontowf1o 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
  Copyright terms: Public domain W3C validator