Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . 5
⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸–1-1-onto→𝐾) |
2 | 1 | ad2antlr 724 |
. . . 4
⊢
(((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → 𝑔:𝐸–1-1-onto→𝐾) |
3 | | f1ocnvdm 7157 |
. . . 4
⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) |
4 | 2, 3 | sylan 580 |
. . 3
⊢
((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) |
5 | | uspgrupgr 27546 |
. . . . . . 7
⊢ (𝐴 ∈ USPGraph → 𝐴 ∈
UPGraph) |
6 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph) → 𝐴 ∈
UPGraph) |
7 | 6 | ad4antr 729 |
. . . . 5
⊢
((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → 𝐴 ∈ UPGraph) |
8 | | isomushgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐴) |
9 | | isomushgr.e |
. . . . . 6
⊢ 𝐸 = (Edg‘𝐴) |
10 | 8, 9 | upgredg 27507 |
. . . . 5
⊢ ((𝐴 ∈ UPGraph ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦}) |
11 | 7, 10 | sylan 580 |
. . . 4
⊢
(((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦}) |
12 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸 ↔ {𝑥, 𝑦} ∈ 𝐸)) |
13 | 12 | biimpd 228 |
. . . . . . . . . 10
⊢ ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸)) |
14 | 13 | com12 32 |
. . . . . . . . 9
⊢ ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸 → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → {𝑥, 𝑦} ∈ 𝐸)) |
15 | 14 | ad2antlr 724 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → {𝑥, 𝑦} ∈ 𝐸)) |
16 | 15 | imp 407 |
. . . . . . 7
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦}) → {𝑥, 𝑦} ∈ 𝐸) |
17 | 1 | ad6antlr 734 |
. . . . . . . . . . 11
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → 𝑔:𝐸–1-1-onto→𝐾) |
18 | | simpr 485 |
. . . . . . . . . . 11
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → {𝑥, 𝑦} ∈ 𝐸) |
19 | | simpr 485 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) |
20 | 19 | ad5ant12 753 |
. . . . . . . . . . 11
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) |
21 | 17, 18, 20 | 3jca 1127 |
. . . . . . . . . 10
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑔:𝐸–1-1-onto→𝐾 ∧ {𝑥, 𝑦} ∈ 𝐸 ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾)) |
22 | | f1ocnvfvb 7151 |
. . . . . . . . . 10
⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ {𝑥, 𝑦} ∈ 𝐸 ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦})) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦})) |
24 | | imaeq2 5965 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = {𝑥, 𝑦} → (𝑓 “ 𝑒) = (𝑓 “ {𝑥, 𝑦})) |
25 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = {𝑥, 𝑦} → (𝑔‘𝑒) = (𝑔‘{𝑥, 𝑦})) |
26 | 24, 25 | eqeq12d 2754 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑥, 𝑦} → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}))) |
27 | 26 | rspccv 3558 |
. . . . . . . . . . . . . 14
⊢
(∀𝑒 ∈
𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}))) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}))) |
29 | 28 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}))) |
30 | 29 | ad4antr 729 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({𝑥, 𝑦} ∈ 𝐸 → (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}))) |
31 | 30 | imp 407 |
. . . . . . . . . 10
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦})) |
32 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ ((𝑔‘{𝑥, 𝑦}) = (𝑓 “ {𝑥, 𝑦}) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)})) |
33 | 32 | eqcoms 2746 |
. . . . . . . . . . . 12
⊢ ((𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦}) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)})) |
34 | 33 | adantl 482 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) ∧ (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦})) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)})) |
35 | | f1ofn 6717 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:𝑉–1-1-onto→𝑊 → 𝑓 Fn 𝑉) |
36 | 35 | ad6antlr 734 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑓 Fn 𝑉) |
37 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝑉) |
39 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
40 | 39 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑦 ∈ 𝑉) |
41 | 36, 38, 40 | 3jca 1127 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑓 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑓 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
43 | | fnimapr 6852 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑥), (𝑓‘𝑦)}) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → (𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑥), (𝑓‘𝑦)}) |
45 | 44 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ {(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)})) |
46 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑥) ∈ V |
47 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑦) ∈ V |
48 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑎) ∈ V |
49 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓‘𝑏) ∈ V |
50 | 46, 47, 48, 49 | preq12b 4781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} ↔ (((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) ∨ ((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎)))) |
51 | | f1of1 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:𝑉–1-1-onto→𝑊 → 𝑓:𝑉–1-1→𝑊) |
52 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
53 | 52, 37 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉)) |
54 | | f1veqaeq 7130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓:𝑉–1-1→𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉)) → ((𝑓‘𝑥) = (𝑓‘𝑎) → 𝑥 = 𝑎)) |
55 | 51, 53, 54 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑓‘𝑥) = (𝑓‘𝑎) → 𝑥 = 𝑎)) |
56 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
57 | 56, 39 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑦 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
58 | | f1veqaeq 7130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓:𝑉–1-1→𝑊 ∧ (𝑦 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑓‘𝑦) = (𝑓‘𝑏) → 𝑦 = 𝑏)) |
59 | 51, 57, 58 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑓‘𝑦) = (𝑓‘𝑏) → 𝑦 = 𝑏)) |
60 | 55, 59 | anim12d 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) → (𝑥 = 𝑎 ∧ 𝑦 = 𝑏))) |
61 | 60 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) ∧ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊)) → (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) |
62 | 61 | orcd 870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) ∧ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊)) → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎))) |
63 | 62 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎)))) |
64 | 56, 37 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
65 | | f1veqaeq 7130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓:𝑉–1-1→𝑊 ∧ (𝑥 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑓‘𝑥) = (𝑓‘𝑏) → 𝑥 = 𝑏)) |
66 | 51, 64, 65 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑓‘𝑥) = (𝑓‘𝑏) → 𝑥 = 𝑏)) |
67 | 52, 39 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑦 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉)) |
68 | | f1veqaeq 7130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓:𝑉–1-1→𝑊 ∧ (𝑦 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉)) → ((𝑓‘𝑦) = (𝑓‘𝑎) → 𝑦 = 𝑎)) |
69 | 51, 67, 68 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑓‘𝑦) = (𝑓‘𝑎) → 𝑦 = 𝑎)) |
70 | 66, 69 | anim12d 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎)) → (𝑥 = 𝑏 ∧ 𝑦 = 𝑎))) |
71 | 70 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎)) ∧ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊)) → (𝑥 = 𝑏 ∧ 𝑦 = 𝑎)) |
72 | 71 | olcd 871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎)) ∧ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊)) → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎))) |
73 | 72 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎)) → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎)))) |
74 | 63, 73 | jaoi 854 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) ∨ ((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎))) → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎)))) |
75 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑥 ∈ V |
76 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑦 ∈ V |
77 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑎 ∈ V |
78 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑏 ∈ V |
79 | 75, 76, 77, 78 | preq12b 4781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝑥, 𝑦} = {𝑎, 𝑏} ↔ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) ∨ (𝑥 = 𝑏 ∧ 𝑦 = 𝑎))) |
80 | 74, 79 | syl6ibr 251 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑓‘𝑥) = (𝑓‘𝑎) ∧ (𝑓‘𝑦) = (𝑓‘𝑏)) ∨ ((𝑓‘𝑥) = (𝑓‘𝑏) ∧ (𝑓‘𝑦) = (𝑓‘𝑎))) → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → {𝑥, 𝑦} = {𝑎, 𝑏})) |
81 | 50, 80 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → {𝑥, 𝑦} = {𝑎, 𝑏})) |
82 | 81 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏})) |
83 | 82 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:𝑉–1-1-onto→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏}))) |
84 | 83 | expd 416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑉–1-1-onto→𝑊 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏})))) |
85 | 84 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏})))) |
86 | 85 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏}))) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏}))) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑥, 𝑦} = {𝑎, 𝑏}))) |
89 | 88 | imp31 418 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)}) → {𝑥, 𝑦} = {𝑎, 𝑏}) |
90 | 89 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)}) → ({𝑥, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)) |
91 | 90 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)}) → ({𝑥, 𝑦} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) |
92 | 91 | impancom 452 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ({(𝑓‘𝑥), (𝑓‘𝑦)} = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑎, 𝑏} ∈ 𝐸)) |
93 | 45, 92 | sylbid 239 |
. . . . . . . . . . . 12
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑎, 𝑏} ∈ 𝐸)) |
94 | 93 | adantr 481 |
. . . . . . . . . . 11
⊢
((((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) ∧ (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦})) → ((𝑓 “ {𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑎, 𝑏} ∈ 𝐸)) |
95 | 34, 94 | sylbid 239 |
. . . . . . . . . 10
⊢
((((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) ∧ (𝑓 “ {𝑥, 𝑦}) = (𝑔‘{𝑥, 𝑦})) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑎, 𝑏} ∈ 𝐸)) |
96 | 31, 95 | mpdan 684 |
. . . . . . . . 9
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((𝑔‘{𝑥, 𝑦}) = {(𝑓‘𝑎), (𝑓‘𝑏)} → {𝑎, 𝑏} ∈ 𝐸)) |
97 | 23, 96 | sylbird 259 |
. . . . . . . 8
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ {𝑥, 𝑦} ∈ 𝐸) → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → {𝑎, 𝑏} ∈ 𝐸)) |
98 | 97 | impancom 452 |
. . . . . . 7
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦}) → ({𝑥, 𝑦} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) |
99 | 16, 98 | mpd 15 |
. . . . . 6
⊢
(((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦}) → {𝑎, 𝑏} ∈ 𝐸) |
100 | 99 | ex 413 |
. . . . 5
⊢
((((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → {𝑎, 𝑏} ∈ 𝐸)) |
101 | 100 | rexlimdvva 3223 |
. . . 4
⊢
(((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) = {𝑥, 𝑦} → {𝑎, 𝑏} ∈ 𝐸)) |
102 | 11, 101 | mpd 15 |
. . 3
⊢
(((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) ∧ (◡𝑔‘{(𝑓‘𝑎), (𝑓‘𝑏)}) ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸) |
103 | 4, 102 | mpdan 684 |
. 2
⊢
((((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾) → {𝑎, 𝑏} ∈ 𝐸) |
104 | 103 | ex 413 |
1
⊢
(((((𝐴 ∈
USPGraph ∧ 𝐵 ∈
USPGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ({(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾 → {𝑎, 𝑏} ∈ 𝐸)) |