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 47811
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 47810 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
653expa 1117 . . . 4 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
7 simprl 771 . . . . . . 7 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → 𝐹:𝑉1-1-onto𝑊)
8 imaeq2 6076 . . . . . . . . . . . . . . . 16 (𝑒 = {𝑥, 𝑦} → (𝐹𝑒) = (𝐹 “ {𝑥, 𝑦}))
9 eqidd 2736 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉1-1-onto𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑒𝐸 ↦ (𝐹𝑒)))
10 simpr 484 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉1-1-onto𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸)
11 f1ofun 6851 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑉1-1-onto𝑊 → Fun 𝐹)
12 zfpair2 5439 . . . . . . . . . . . . . . . . . 18 {𝑥, 𝑦} ∈ V
13 funimaexg 6654 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹 ∧ {𝑥, 𝑦} ∈ V) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
1411, 12, 13sylancl 586 . . . . . . . . . . . . . . . . 17 (𝐹:𝑉1-1-onto𝑊 → (𝐹 “ {𝑥, 𝑦}) ∈ V)
1514adantr 480 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉1-1-onto𝑊 ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ V)
168, 9, 10, 15fvmptd4 7040 . . . . . . . . . . . . . . 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 6849 . . . . . . . . . . . . . . . 16 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 → (𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷)
2221ad2antll 729 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → (𝑒𝐸 ↦ (𝐹𝑒)):𝐸𝐷)
23 ax-1 6 . . . . . . . . . . . . . . . . 17 (∅ ∉ 𝐷 → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
24 nnel 3054 . . . . . . . . . . . . . . . . . 18 (¬ ∅ ∉ 𝐷 ↔ ∅ ∈ 𝐷)
25 uspgruhgr 29216 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph)
26 uhgredgn0 29160 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐻 ∈ UHGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
2725, 26sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}))
28 neldifsn 4797 . . . . . . . . . . . . . . . . . . . . . 22 ¬ ∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅})
2928pm2.21i 119 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) → ∅ ∉ 𝐷)
3027, 29syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ USPGraph ∧ ∅ ∈ (Edg‘𝐻)) → ∅ ∉ 𝐷)
3130expcom 413 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ (Edg‘𝐻) → (𝐻 ∈ USPGraph → ∅ ∉ 𝐷))
3231, 4eleq2s 2857 . . . . . . . . . . . . . . . . . 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 7106 . . . . . . . . . . . . 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 2840 . . . . . . . . . 10 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷)
42 imaeq2 6076 . . . . . . . . . . . . 13 (𝑧 = (𝐹 “ {𝑥, 𝑦}) → (𝐹𝑧) = (𝐹 “ (𝐹 “ {𝑥, 𝑦})))
43 imaeq2 6076 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑦 → (𝐹𝑒) = (𝐹𝑦))
4443cbvmptv 5261 . . . . . . . . . . . . . . . . 17 (𝑒𝐸 ↦ (𝐹𝑒)) = (𝑦𝐸 ↦ (𝐹𝑦))
45 f1oeq1 6837 . . . . . . . . . . . . . . . . 17 ((𝑒𝐸 ↦ (𝐹𝑒)) = (𝑦𝐸 ↦ (𝐹𝑦)) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 ↔ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷))
4644, 45mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 ↔ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷))
47 imaeq2 6076 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑥 → (𝐹𝑒) = (𝐹𝑥))
4847cbvmptv 5261 . . . . . . . . . . . . . . . . . 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 29216 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
52 uhgredgss 29163 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))
53 difss2 4148 . . . . . . . . . . . . . . . . . . . . . 22 ((Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}) → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
5451, 52, 533syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ∈ USPGraph → (Edg‘𝐺) ⊆ 𝒫 (Vtx‘𝐺))
551pweqi 4621 . . . . . . . . . . . . . . . . . . . . 21 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)
5654, 3, 553sstr4g 4041 . . . . . . . . . . . . . . . . . . . 20 (𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉)
5756adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐸 ⊆ 𝒫 𝑉)
5857ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝐸 ⊆ 𝒫 𝑉)
59 f1ofo 6856 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷 → (𝑦𝐸 ↦ (𝐹𝑦)):𝐸onto𝐷)
6044rneqi 5951 . . . . . . . . . . . . . . . . . . . . . 22 ran (𝑒𝐸 ↦ (𝐹𝑒)) = ran (𝑦𝐸 ↦ (𝐹𝑦))
61 forn 6824 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐸 ↦ (𝐹𝑦)):𝐸onto𝐷 → ran (𝑦𝐸 ↦ (𝐹𝑦)) = 𝐷)
6260, 61eqtrid 2787 . . . . . . . . . . . . . . . . . . . . 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 29163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻 ∈ UHGraph → (Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}))
66 difss2 4148 . . . . . . . . . . . . . . . . . . . . . . 23 ((Edg‘𝐻) ⊆ (𝒫 (Vtx‘𝐻) ∖ {∅}) → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
6725, 65, 663syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻 ∈ USPGraph → (Edg‘𝐻) ⊆ 𝒫 (Vtx‘𝐻))
682pweqi 4621 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 𝑊 = 𝒫 (Vtx‘𝐻)
6967, 4, 683sstr4g 4041 . . . . . . . . . . . . . . . . . . . . 21 (𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊)
7069adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → 𝐷 ⊆ 𝒫 𝑊)
7170ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝐷 ⊆ 𝒫 𝑊)
7264, 71eqsstrd 4034 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → ran (𝑒𝐸 ↦ (𝐹𝑒)) ⊆ 𝒫 𝑊)
731fvexi 6921 . . . . . . . . . . . . . . . . . . 19 𝑉 ∈ V
7473a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑦𝐸 ↦ (𝐹𝑦)):𝐸1-1-onto𝐷) → 𝑉 ∈ V)
7548, 50, 58, 72, 74mptcnfimad 8010 . . . . . . . . . . . . . . . . 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 6856 . . . . . . . . . . . . . . . . . 18 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 → (𝑒𝐸 ↦ (𝐹𝑒)):𝐸onto𝐷)
81 forn 6824 . . . . . . . . . . . . . . . . . . 19 ((𝑒𝐸 ↦ (𝐹𝑒)):𝐸onto𝐷 → ran (𝑒𝐸 ↦ (𝐹𝑒)) = 𝐷)
8281eqcomd 2741 . . . . . . . . . . . . . . . . . 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 2825 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒𝐸 ↦ (𝐹𝑒))))
8786biimpa 476 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ {𝑥, 𝑦}) ∈ ran (𝑒𝐸 ↦ (𝐹𝑒)))
88 dff1o2 6854 . . . . . . . . . . . . . . . . 17 (𝐹:𝑉1-1-onto𝑊 ↔ (𝐹 Fn 𝑉 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝑊))
8988simp2bi 1145 . . . . . . . . . . . . . . . 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 6654 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
9391, 92sylan 580 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ V)
9442, 79, 87, 93fvmptd4 7040 . . . . . . . . . . . 12 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ((𝑒𝐸 ↦ (𝐹𝑒))‘(𝐹 “ {𝑥, 𝑦})) = (𝐹 “ (𝐹 “ {𝑥, 𝑦})))
95 simplrr 778 . . . . . . . . . . . . 13 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)
96 f1ocnvdm 7305 . . . . . . . . . . . . 13 (((𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷 ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ((𝑒𝐸 ↦ (𝐹𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
9795, 96sylan 580 . . . . . . . . . . . 12 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → ((𝑒𝐸 ↦ (𝐹𝑒))‘(𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
9894, 97eqeltrrd 2840 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) ∧ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) ∈ 𝐸)
99 f1of1 6848 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝑊𝐹:𝑉1-1𝑊)
10099ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) → 𝐹:𝑉1-1𝑊)
101 prssi 4826 . . . . . . . . . . . . . . 15 ((𝑥𝑉𝑦𝑉) → {𝑥, 𝑦} ⊆ 𝑉)
102 f1imacnv 6865 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝑊 ∧ {𝑥, 𝑦} ⊆ 𝑉) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
103100, 101, 102syl2an 596 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 “ (𝐹 “ {𝑥, 𝑦})) = {𝑥, 𝑦})
104103eqcomd 2741 . . . . . . . . . . . . 13 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → {𝑥, 𝑦} = (𝐹 “ (𝐹 “ {𝑥, 𝑦})))
105104eleq1d 2824 . . . . . . . . . . . 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 801 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ (𝐹 “ {𝑥, 𝑦}) ∈ 𝐷))
109 f1ofn 6850 . . . . . . . . . . . . . 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 6992 . . . . . . . . . . 11 ((𝐹 Fn 𝑉𝑥𝑉𝑦𝑉) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹𝑥), (𝐹𝑦)})
115113, 114syl 17 . . . . . . . . . 10 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → (𝐹 “ {𝑥, 𝑦}) = {(𝐹𝑥), (𝐹𝑦)})
116115eleq1d 2824 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ((𝐹 “ {𝑥, 𝑦}) ∈ 𝐷 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))
117108, 116bitrd 279 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)) ∧ (𝑥𝑉𝑦𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹𝑥), (𝐹𝑦)} ∈ 𝐷))
118117ralrimivva 3200 . . . . . . 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 1537  wcel 2106  wnel 3044  wral 3059  Vcvv 3478  cdif 3960  wss 3963  c0 4339  𝒫 cpw 4605  {csn 4631  {cpr 4633  cmpt 5231  ccnv 5688  ran crn 5690  cima 5692  Fun wfun 6557   Fn wfn 6558  wf 6559  1-1wf1 6560  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  Vtxcvtx 29028  Edgcedg 29079  UHGraphcuhgr 29088  USPGraphcuspgr 29180   GraphIso cgrim 47799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8867  df-edg 29080  df-uhgr 29090  df-upgr 29114  df-uspgr 29182  df-grim 47802
This theorem is referenced by:  isuspgrim  47813
  Copyright terms: Public domain W3C validator