Step | Hyp | Ref
| Expression |
1 | | isomushgr.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐴) |
2 | | isomushgr.w |
. . 3
⊢ 𝑊 = (Vtx‘𝐵) |
3 | | isomushgr.e |
. . 3
⊢ 𝐸 = (Edg‘𝐴) |
4 | | isomushgr.k |
. . 3
⊢ 𝐾 = (Edg‘𝐵) |
5 | | isomuspgrlem2.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)) |
6 | | isomuspgrlem2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ USPGraph) |
7 | | isomuspgrlem2.f |
. . 3
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊) |
8 | | isomuspgrlem2.i |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | isomuspgrlem2b 45238 |
. 2
⊢ (𝜑 → 𝐺:𝐸⟶𝐾) |
10 | | isomuspgrlem2.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ USPGraph) |
11 | | uspgrupgr 27535 |
. . . . . 6
⊢ (𝐵 ∈ USPGraph → 𝐵 ∈
UPGraph) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ UPGraph) |
13 | 2, 4 | upgredg 27496 |
. . . . 5
⊢ ((𝐵 ∈ UPGraph ∧ 𝑦 ∈ 𝐾) → ∃𝑐 ∈ 𝑊 ∃𝑑 ∈ 𝑊 𝑦 = {𝑐, 𝑑}) |
14 | 12, 13 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ∃𝑐 ∈ 𝑊 ∃𝑑 ∈ 𝑊 𝑦 = {𝑐, 𝑑}) |
15 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑐, 𝑑} → (𝑦 ∈ 𝐾 ↔ {𝑐, 𝑑} ∈ 𝐾)) |
16 | 15 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑦 = {𝑐, 𝑑} → ((𝜑 ∧ 𝑦 ∈ 𝐾) ↔ (𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾))) |
17 | | f1ofo 6717 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–onto→𝑊) |
18 | 7, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑉–onto→𝑊) |
19 | | foelrn 6976 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝑉–onto→𝑊 ∧ 𝑐 ∈ 𝑊) → ∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚)) |
20 | 18, 19 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑊) → ∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚)) |
21 | 20 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑐 ∈ 𝑊 → ∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚))) |
22 | | foelrn 6976 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝑉–onto→𝑊 ∧ 𝑑 ∈ 𝑊) → ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛)) |
23 | 18, 22 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑊) → ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛)) |
24 | 23 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑑 ∈ 𝑊 → ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛))) |
25 | 21, 24 | anim12d 609 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊) → (∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚) ∧ ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛)))) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) → ((𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊) → (∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚) ∧ ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛)))) |
27 | 26 | imp 407 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚) ∧ ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛))) |
28 | | preq12 4673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 = (𝐹‘𝑚) ∧ 𝑑 = (𝐹‘𝑛)) → {𝑐, 𝑑} = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
29 | 28 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → {𝑐, 𝑑} = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
30 | 29 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → ({𝑐, 𝑑} ∈ 𝐾 ↔ {(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾)) |
31 | | preq1 4671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑚 → {𝑎, 𝑏} = {𝑚, 𝑏}) |
32 | 31 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = 𝑚 → ({𝑎, 𝑏} ∈ 𝐸 ↔ {𝑚, 𝑏} ∈ 𝐸)) |
33 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = 𝑚 → (𝐹‘𝑎) = (𝐹‘𝑚)) |
34 | 33 | preq1d 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑚 → {(𝐹‘𝑎), (𝐹‘𝑏)} = {(𝐹‘𝑚), (𝐹‘𝑏)}) |
35 | 34 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = 𝑚 → ({(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾 ↔ {(𝐹‘𝑚), (𝐹‘𝑏)} ∈ 𝐾)) |
36 | 32, 35 | bibi12d 346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = 𝑚 → (({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) ↔ ({𝑚, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑚), (𝐹‘𝑏)} ∈ 𝐾))) |
37 | | preq2 4672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑏 = 𝑛 → {𝑚, 𝑏} = {𝑚, 𝑛}) |
38 | 37 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑏 = 𝑛 → ({𝑚, 𝑏} ∈ 𝐸 ↔ {𝑚, 𝑛} ∈ 𝐸)) |
39 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = 𝑛 → (𝐹‘𝑏) = (𝐹‘𝑛)) |
40 | 39 | preq2d 4678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑏 = 𝑛 → {(𝐹‘𝑚), (𝐹‘𝑏)} = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
41 | 40 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑏 = 𝑛 → ({(𝐹‘𝑚), (𝐹‘𝑏)} ∈ 𝐾 ↔ {(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾)) |
42 | 38, 41 | bibi12d 346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 = 𝑛 → (({𝑚, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑚), (𝐹‘𝑏)} ∈ 𝐾) ↔ ({𝑚, 𝑛} ∈ 𝐸 ↔ {(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾))) |
43 | 36, 42 | rspc2va 3572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾)) → ({𝑚, 𝑛} ∈ 𝐸 ↔ {(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾)) |
44 | 43 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾)) → ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 ↔ {𝑚, 𝑛} ∈ 𝐸)) |
45 | 44 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑎 ∈
𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 ↔ {𝑚, 𝑛} ∈ 𝐸)) |
46 | 45 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑎 ∈
𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 → {𝑚, 𝑛} ∈ 𝐸)) |
47 | 46 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑎 ∈
𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝐹‘𝑎), (𝐹‘𝑏)} ∈ 𝐾) → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 → {𝑚, 𝑛} ∈ 𝐸))) |
48 | 8, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 → {𝑚, 𝑛} ∈ 𝐸))) |
49 | 48 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({(𝐹‘𝑚), (𝐹‘𝑛)} ∈ 𝐾 → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝜑 → {𝑚, 𝑛} ∈ 𝐸))) |
50 | 30, 49 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → ({𝑐, 𝑑} ∈ 𝐾 → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝜑 → {𝑚, 𝑛} ∈ 𝐸)))) |
51 | 50 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ({𝑐, 𝑑} ∈ 𝐾 → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → {𝑚, 𝑛} ∈ 𝐸)))) |
52 | 51 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → {𝑚, 𝑛} ∈ 𝐸))) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → {𝑚, 𝑛} ∈ 𝐸))) |
54 | 53 | imp31 418 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) → {𝑚, 𝑛} ∈ 𝐸) |
55 | | imaeq2 5960 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = {𝑚, 𝑛} → (𝐹 “ 𝑒) = (𝐹 “ {𝑚, 𝑛})) |
56 | | f1ofn 6711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹 Fn 𝑉) |
57 | 7, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹 Fn 𝑉) |
58 | 57 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → 𝐹 Fn 𝑉) |
59 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → 𝑚 ∈ 𝑉) |
60 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → 𝑛 ∈ 𝑉) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → 𝑛 ∈ 𝑉) |
62 | 58, 59, 61 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → (𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) → (𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) |
64 | | fnimapr 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉) → (𝐹 “ {𝑚, 𝑛}) = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) → (𝐹 “ {𝑚, 𝑛}) = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
66 | 55, 65 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) ∧ 𝑒 = {𝑚, 𝑛}) → (𝐹 “ 𝑒) = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
67 | 66 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) ∧ 𝑒 = {𝑚, 𝑛}) → ({𝑐, 𝑑} = (𝐹 “ 𝑒) ↔ {𝑐, 𝑑} = {(𝐹‘𝑚), (𝐹‘𝑛)})) |
68 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) → {𝑐, 𝑑} = {(𝐹‘𝑚), (𝐹‘𝑛)}) |
69 | 54, 67, 68 | rspcedvd 3564 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) ∧ (𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚))) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)) |
70 | 69 | ex 413 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ (𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉)) → ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
71 | 70 | anassrs 468 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑚 ∈ 𝑉) ∧ 𝑛 ∈ 𝑉) → ((𝑑 = (𝐹‘𝑛) ∧ 𝑐 = (𝐹‘𝑚)) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
72 | 71 | expd 416 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑚 ∈ 𝑉) ∧ 𝑛 ∈ 𝑉) → (𝑑 = (𝐹‘𝑛) → (𝑐 = (𝐹‘𝑚) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)))) |
73 | 72 | rexlimdva 3212 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑚 ∈ 𝑉) → (∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛) → (𝑐 = (𝐹‘𝑚) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)))) |
74 | 73 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑚 ∈ 𝑉) → (𝑐 = (𝐹‘𝑚) → (∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)))) |
75 | 74 | rexlimdva 3212 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚) → (∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)))) |
76 | 75 | impd 411 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → ((∃𝑚 ∈ 𝑉 𝑐 = (𝐹‘𝑚) ∧ ∃𝑛 ∈ 𝑉 𝑑 = (𝐹‘𝑛)) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
77 | 27, 76 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)) |
78 | 77 | ex 413 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ {𝑐, 𝑑} ∈ 𝐾) → ((𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
79 | 16, 78 | syl6bi 252 |
. . . . . . . . 9
⊢ (𝑦 = {𝑐, 𝑑} → ((𝜑 ∧ 𝑦 ∈ 𝐾) → ((𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)))) |
80 | 79 | impd 411 |
. . . . . . . 8
⊢ (𝑦 = {𝑐, 𝑑} → (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
81 | 80 | impcom 408 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) → ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒)) |
82 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) → 𝑦 = {𝑐, 𝑑}) |
83 | 82 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → 𝑦 = {𝑐, 𝑑}) |
84 | | isomuspgrlem2.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ 𝑋) |
85 | 84 | ad4antr 729 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → 𝐹 ∈ 𝑋) |
86 | 1, 2, 3, 4, 5 | isomuspgrlem2a 45237 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ 𝑋 → ∀𝑦 ∈ 𝐸 (𝐹 “ 𝑦) = (𝐺‘𝑦)) |
87 | 85, 86 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → ∀𝑦 ∈ 𝐸 (𝐹 “ 𝑦) = (𝐺‘𝑦)) |
88 | | imaeq2 5960 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑒 → (𝐹 “ 𝑦) = (𝐹 “ 𝑒)) |
89 | | fveq2 6768 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑒 → (𝐺‘𝑦) = (𝐺‘𝑒)) |
90 | 88, 89 | eqeq12d 2754 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑒 → ((𝐹 “ 𝑦) = (𝐺‘𝑦) ↔ (𝐹 “ 𝑒) = (𝐺‘𝑒))) |
91 | 90 | rspcv 3556 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ 𝐸 → (∀𝑦 ∈ 𝐸 (𝐹 “ 𝑦) = (𝐺‘𝑦) → (𝐹 “ 𝑒) = (𝐺‘𝑒))) |
92 | | eqcom 2745 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑒) = (𝐹 “ 𝑒) ↔ (𝐹 “ 𝑒) = (𝐺‘𝑒)) |
93 | 91, 92 | syl6ibr 251 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ 𝐸 → (∀𝑦 ∈ 𝐸 (𝐹 “ 𝑦) = (𝐺‘𝑦) → (𝐺‘𝑒) = (𝐹 “ 𝑒))) |
94 | 93 | adantl 482 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → (∀𝑦 ∈ 𝐸 (𝐹 “ 𝑦) = (𝐺‘𝑦) → (𝐺‘𝑒) = (𝐹 “ 𝑒))) |
95 | 87, 94 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → (𝐺‘𝑒) = (𝐹 “ 𝑒)) |
96 | 83, 95 | eqeq12d 2754 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) ∧ 𝑒 ∈ 𝐸) → (𝑦 = (𝐺‘𝑒) ↔ {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
97 | 96 | rexbidva 3224 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) → (∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒) ↔ ∃𝑒 ∈ 𝐸 {𝑐, 𝑑} = (𝐹 “ 𝑒))) |
98 | 81, 97 | mpbird 256 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) ∧ 𝑦 = {𝑐, 𝑑}) → ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒)) |
99 | 98 | ex 413 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ (𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊)) → (𝑦 = {𝑐, 𝑑} → ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒))) |
100 | 99 | rexlimdvva 3222 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (∃𝑐 ∈ 𝑊 ∃𝑑 ∈ 𝑊 𝑦 = {𝑐, 𝑑} → ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒))) |
101 | 14, 100 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒)) |
102 | 101 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐾 ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒)) |
103 | | dffo3 6972 |
. 2
⊢ (𝐺:𝐸–onto→𝐾 ↔ (𝐺:𝐸⟶𝐾 ∧ ∀𝑦 ∈ 𝐾 ∃𝑒 ∈ 𝐸 𝑦 = (𝐺‘𝑒))) |
104 | 9, 102, 103 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐺:𝐸–onto→𝐾) |