| 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→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))) |