Step | Hyp | Ref
| Expression |
1 | | isomuspgrlem2.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ USPGraph) |
2 | | uspgrupgr 27546 |
. . . . . 6
⊢ (𝐴 ∈ USPGraph → 𝐴 ∈
UPGraph) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ UPGraph) |
4 | | isomushgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐴) |
5 | | isomushgr.e |
. . . . . 6
⊢ 𝐸 = (Edg‘𝐴) |
6 | 4, 5 | upgredg 27507 |
. . . . 5
⊢ ((𝐴 ∈ UPGraph ∧ 𝑥 ∈ 𝐸) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 𝑥 = {𝑐, 𝑑}) |
7 | 3, 6 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐸) → ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 𝑥 = {𝑐, 𝑑}) |
8 | | isomuspgrlem2.i |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾)) |
9 | | preq12 4671 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → {𝑎, 𝑏} = {𝑐, 𝑑}) |
10 | 9 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {𝑐, 𝑑} ∈ 𝐸)) |
11 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐)) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝐹‘𝑎) = (𝐹‘𝑐)) |
13 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑)) |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝐹‘𝑏) = (𝐹‘𝑑)) |
15 | 12, 14 | preq12d 4677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → {(𝐹‘𝑎), (𝐹‘𝑏)} = {(𝐹‘𝑐), (𝐹‘𝑑)}) |
16 | 15 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ({(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾)) |
17 | 10, 16 | bibi12d 346 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) ↔ ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾))) |
18 | 17 | rspc2gv 3569 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾))) |
19 | 8, 18 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾))) |
20 | 19 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾))) |
21 | 20 | imp 407 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾)) |
22 | | bicom 221 |
. . . . . . . . . . . . 13
⊢ (({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾) ↔ ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 ↔ {𝑐, 𝑑} ∈ 𝐸)) |
23 | | bianir 1056 |
. . . . . . . . . . . . . 14
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 ↔ {𝑐, 𝑑} ∈ 𝐸)) → {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾) |
24 | 23 | ex 413 |
. . . . . . . . . . . . 13
⊢ ({𝑐, 𝑑} ∈ 𝐸 → (({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 ↔ {𝑐, 𝑑} ∈ 𝐸) → {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾)) |
25 | 22, 24 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ ({𝑐, 𝑑} ∈ 𝐸 → (({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾) → {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾)) |
26 | | isomuspgrlem2.f |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊) |
27 | | f1ofn 6717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 Fn 𝑉) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) → 𝐹 Fn 𝑉) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝐹 Fn 𝑉) |
31 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑐 ∈ 𝑉) |
32 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑑 ∈ 𝑉) |
33 | 30, 31, 32 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) |
35 | | fnimapr 6852 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → (𝐹 “ {𝑐, 𝑑}) = {(𝐹‘𝑐), (𝐹‘𝑑)}) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝐹 “ {𝑐, 𝑑}) = {(𝐹‘𝑐), (𝐹‘𝑑)}) |
37 | 36 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → {(𝐹‘𝑐), (𝐹‘𝑑)} = (𝐹 “ {𝑐, 𝑑})) |
38 | 37 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 ↔ (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾)) |
39 | 38 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢ (({𝑐, 𝑑} ∈ 𝐸 ∧ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾)) |
40 | 39 | ex 413 |
. . . . . . . . . . . . 13
⊢ ({𝑐, 𝑑} ∈ 𝐸 → (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
41 | 40 | com23 86 |
. . . . . . . . . . . 12
⊢ ({𝑐, 𝑑} ∈ 𝐸 → ({(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾 → (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
42 | 25, 41 | syld 47 |
. . . . . . . . . . 11
⊢ ({𝑐, 𝑑} ∈ 𝐸 → (({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾) → (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
43 | 42 | com13 88 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝐹‘𝑐), (𝐹‘𝑑)} ∈ 𝐾) → ({𝑐, 𝑑} ∈ 𝐸 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
44 | 21, 43 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → ({𝑐, 𝑑} ∈ 𝐸 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾)) |
45 | | eleq1 2826 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑐, 𝑑} → (𝑥 ∈ 𝐸 ↔ {𝑐, 𝑑} ∈ 𝐸)) |
46 | | imaeq2 5965 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑐, 𝑑} → (𝐹 “ 𝑥) = (𝐹 “ {𝑐, 𝑑})) |
47 | 46 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑐, 𝑑} → ((𝐹 “ 𝑥) ∈ 𝐾 ↔ (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾)) |
48 | 45, 47 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑐, 𝑑} → ((𝑥 ∈ 𝐸 → (𝐹 “ 𝑥) ∈ 𝐾) ↔ ({𝑐, 𝑑} ∈ 𝐸 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
49 | 48 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) → ((𝑥 ∈ 𝐸 → (𝐹 “ 𝑥) ∈ 𝐾) ↔ ({𝑐, 𝑑} ∈ 𝐸 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
50 | 49 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → ((𝑥 ∈ 𝐸 → (𝐹 “ 𝑥) ∈ 𝐾) ↔ ({𝑐, 𝑑} ∈ 𝐸 → (𝐹 “ {𝑐, 𝑑}) ∈ 𝐾))) |
51 | 44, 50 | mpbird 256 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = {𝑐, 𝑑}) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑥 ∈ 𝐸 → (𝐹 “ 𝑥) ∈ 𝐾)) |
52 | 51 | exp31 420 |
. . . . . . 7
⊢ (𝜑 → (𝑥 = {𝑐, 𝑑} → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → (𝑥 ∈ 𝐸 → (𝐹 “ 𝑥) ∈ 𝐾)))) |
53 | 52 | com24 95 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐸 → ((𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉) → (𝑥 = {𝑐, 𝑑} → (𝐹 “ 𝑥) ∈ 𝐾)))) |
54 | 53 | imp31 418 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐸) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑥 = {𝑐, 𝑑} → (𝐹 “ 𝑥) ∈ 𝐾)) |
55 | 54 | rexlimdvva 3223 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐸) → (∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 𝑥 = {𝑐, 𝑑} → (𝐹 “ 𝑥) ∈ 𝐾)) |
56 | 7, 55 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐸) → (𝐹 “ 𝑥) ∈ 𝐾) |
57 | 56 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐸 (𝐹 “ 𝑥) ∈ 𝐾) |
58 | | isomuspgrlem2.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)) |
59 | 58 | fmpt 6984 |
. 2
⊢
(∀𝑥 ∈
𝐸 (𝐹 “ 𝑥) ∈ 𝐾 ↔ 𝐺:𝐸⟶𝐾) |
60 | 57, 59 | sylib 217 |
1
⊢ (𝜑 → 𝐺:𝐸⟶𝐾) |