Proof of Theorem fnwelem
Step | Hyp | Ref
| Expression |
1 | | fnwe.2 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵) |
3 | | simpr 476 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
4 | | opelxp 5070 |
. . . . . 6
⊢
(〈(𝐹‘𝑧), 𝑧〉 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑧) ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) |
5 | 2, 3, 4 | sylanbrc 695 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → 〈(𝐹‘𝑧), 𝑧〉 ∈ (𝐵 × 𝐴)) |
6 | | fnwelem.7 |
. . . . 5
⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ 〈(𝐹‘𝑧), 𝑧〉) |
7 | 5, 6 | fmptd 6292 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐺:𝐴⟶(𝐵 × 𝐴)) |
8 | | frn 5966 |
. . . 4
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ran 𝐺 ⊆ (𝐵 × 𝐴)) |
9 | 1, 7, 8 | 3syl 18 |
. . 3
⊢ (𝜑 → ran 𝐺 ⊆ (𝐵 × 𝐴)) |
10 | | fnwe.3 |
. . . 4
⊢ (𝜑 → 𝑅 We 𝐵) |
11 | | fnwe.4 |
. . . 4
⊢ (𝜑 → 𝑆 We 𝐴) |
12 | | fnwelem.6 |
. . . . 5
⊢ 𝑄 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd
‘𝑢)𝑆(2nd ‘𝑣))))} |
13 | 12 | wexp 7178 |
. . . 4
⊢ ((𝑅 We 𝐵 ∧ 𝑆 We 𝐴) → 𝑄 We (𝐵 × 𝐴)) |
14 | 10, 11, 13 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑄 We (𝐵 × 𝐴)) |
15 | | wess 5025 |
. . 3
⊢ (ran
𝐺 ⊆ (𝐵 × 𝐴) → (𝑄 We (𝐵 × 𝐴) → 𝑄 We ran 𝐺)) |
16 | 9, 14, 15 | sylc 63 |
. 2
⊢ (𝜑 → 𝑄 We ran 𝐺) |
17 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
18 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥) |
19 | 17, 18 | opeq12d 4348 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → 〈(𝐹‘𝑧), 𝑧〉 = 〈(𝐹‘𝑥), 𝑥〉) |
20 | | opex 4859 |
. . . . . . . . . . . 12
⊢
〈(𝐹‘𝑥), 𝑥〉 ∈ V |
21 | 19, 6, 20 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (𝐺‘𝑥) = 〈(𝐹‘𝑥), 𝑥〉) |
22 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
23 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) |
24 | 22, 23 | opeq12d 4348 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → 〈(𝐹‘𝑧), 𝑧〉 = 〈(𝐹‘𝑦), 𝑦〉) |
25 | | opex 4859 |
. . . . . . . . . . . 12
⊢
〈(𝐹‘𝑦), 𝑦〉 ∈ V |
26 | 24, 6, 25 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → (𝐺‘𝑦) = 〈(𝐹‘𝑦), 𝑦〉) |
27 | 21, 26 | eqeqan12d 2626 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐺‘𝑦) ↔ 〈(𝐹‘𝑥), 𝑥〉 = 〈(𝐹‘𝑦), 𝑦〉)) |
28 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
29 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
30 | 28, 29 | opth 4871 |
. . . . . . . . . . 11
⊢
(〈(𝐹‘𝑥), 𝑥〉 = 〈(𝐹‘𝑦), 𝑦〉 ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 = 𝑦)) |
31 | 30 | simprbi 479 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑥), 𝑥〉 = 〈(𝐹‘𝑦), 𝑦〉 → 𝑥 = 𝑦) |
32 | 27, 31 | syl6bi 242 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦)) |
33 | 32 | rgen2a 2960 |
. . . . . . . 8
⊢
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦)) |
35 | | dff13 6416 |
. . . . . . 7
⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) ↔ (𝐺:𝐴⟶(𝐵 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦))) |
36 | 7, 34, 35 | sylanbrc 695 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → 𝐺:𝐴–1-1→(𝐵 × 𝐴)) |
37 | | f1f1orn 6061 |
. . . . . 6
⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → 𝐺:𝐴–1-1-onto→ran
𝐺) |
38 | | f1ocnv 6062 |
. . . . . 6
⊢ (𝐺:𝐴–1-1-onto→ran
𝐺 → ◡𝐺:ran 𝐺–1-1-onto→𝐴) |
39 | 1, 36, 37, 38 | 4syl 19 |
. . . . 5
⊢ (𝜑 → ◡𝐺:ran 𝐺–1-1-onto→𝐴) |
40 | | eqid 2610 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} |
41 | 40 | f1oiso2 6502 |
. . . . . 6
⊢ (◡𝐺:ran 𝐺–1-1-onto→𝐴 → ◡𝐺 Isom 𝑄, {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴)) |
42 | | fnwe.1 |
. . . . . . . 8
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} |
43 | | frel 5963 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → Rel 𝐺) |
44 | | dfrel2 5502 |
. . . . . . . . . . . . . . . 16
⊢ (Rel
𝐺 ↔ ◡◡𝐺 = 𝐺) |
45 | 43, 44 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ◡◡𝐺 = 𝐺) |
46 | 45 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → (◡◡𝐺‘𝑥) = (𝐺‘𝑥)) |
47 | 45 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → (◡◡𝐺‘𝑦) = (𝐺‘𝑦)) |
48 | 46, 47 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦))) |
49 | 7, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦))) |
50 | 49 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦))) |
51 | 21, 26 | breqan12d 4599 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥)𝑄(𝐺‘𝑦) ↔ 〈(𝐹‘𝑥), 𝑥〉𝑄〈(𝐹‘𝑦), 𝑦〉)) |
52 | 51 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐺‘𝑥)𝑄(𝐺‘𝑦) ↔ 〈(𝐹‘𝑥), 𝑥〉𝑄〈(𝐹‘𝑦), 𝑦〉)) |
53 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
54 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
55 | 53, 54 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
56 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐵) |
57 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
58 | 56, 57 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) |
59 | 55, 58 | anim12dan 878 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))) |
60 | 59 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))))) |
61 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (𝑢 ∈ (𝐵 × 𝐴) ↔ 〈(𝐹‘𝑥), 𝑥〉 ∈ (𝐵 × 𝐴))) |
62 | | opelxp 5070 |
. . . . . . . . . . . . . . . 16
⊢
(〈(𝐹‘𝑥), 𝑥〉 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
63 | 61, 62 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (𝑢 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))) |
64 | 63 | anbi1d 737 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ↔ (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)))) |
65 | 28, 29 | op1std 7069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (1st ‘𝑢) = (𝐹‘𝑥)) |
66 | 65 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → ((1st ‘𝑢)𝑅(1st ‘𝑣) ↔ (𝐹‘𝑥)𝑅(1st ‘𝑣))) |
67 | 65 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → ((1st ‘𝑢) = (1st ‘𝑣) ↔ (𝐹‘𝑥) = (1st ‘𝑣))) |
68 | 28, 29 | op2ndd 7070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (2nd ‘𝑢) = 𝑥) |
69 | 68 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → ((2nd ‘𝑢)𝑆(2nd ‘𝑣) ↔ 𝑥𝑆(2nd ‘𝑣))) |
70 | 67, 69 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd
‘𝑢)𝑆(2nd ‘𝑣)) ↔ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)))) |
71 | 66, 70 | orbi12d 742 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd
‘𝑢)𝑆(2nd ‘𝑣))) ↔ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣))))) |
72 | 64, 71 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 〈(𝐹‘𝑥), 𝑥〉 → (((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd
‘𝑢)𝑆(2nd ‘𝑣)))) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)))))) |
73 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (𝑣 ∈ (𝐵 × 𝐴) ↔ 〈(𝐹‘𝑦), 𝑦〉 ∈ (𝐵 × 𝐴))) |
74 | | opelxp 5070 |
. . . . . . . . . . . . . . . 16
⊢
(〈(𝐹‘𝑦), 𝑦〉 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) |
75 | 73, 74 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (𝑣 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))) |
76 | 75 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ↔ (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))) |
77 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑦) ∈ V |
78 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
79 | 77, 78 | op1std 7069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (1st ‘𝑣) = (𝐹‘𝑦)) |
80 | 79 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → ((𝐹‘𝑥)𝑅(1st ‘𝑣) ↔ (𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
81 | 79 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → ((𝐹‘𝑥) = (1st ‘𝑣) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
82 | 77, 78 | op2ndd 7070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (2nd ‘𝑣) = 𝑦) |
83 | 82 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (𝑥𝑆(2nd ‘𝑣) ↔ 𝑥𝑆𝑦)) |
84 | 81, 83 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))) |
85 | 80, 84 | orbi12d 742 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣))) ↔ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))) |
86 | 76, 85 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 〈(𝐹‘𝑦), 𝑦〉 → (((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)))) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))))) |
87 | 20, 25, 72, 86, 12 | brab 4923 |
. . . . . . . . . . . 12
⊢
(〈(𝐹‘𝑥), 𝑥〉𝑄〈(𝐹‘𝑦), 𝑦〉 ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))) |
88 | 60, 87 | syl6rbbr 278 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (〈(𝐹‘𝑥), 𝑥〉𝑄〈(𝐹‘𝑦), 𝑦〉 ↔ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))) |
89 | 50, 52, 88 | 3bitrrd 294 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)) ↔ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))) |
90 | 89 | pm5.32da 671 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦)))) |
91 | 90 | opabbidv 4648 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))}) |
92 | 42, 91 | syl5eq 2656 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))}) |
93 | | isoeq3 6469 |
. . . . . . 7
⊢ (𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} → (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) ↔ ◡𝐺 Isom 𝑄, {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴))) |
94 | 92, 93 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) ↔ ◡𝐺 Isom 𝑄, {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴))) |
95 | 41, 94 | syl5ibr 235 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐺:ran 𝐺–1-1-onto→𝐴 → ◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴))) |
96 | 1, 39, 95 | sylc 63 |
. . . 4
⊢ (𝜑 → ◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴)) |
97 | | isocnv 6480 |
. . . 4
⊢ (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) → ◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺)) |
98 | 96, 97 | syl 17 |
. . 3
⊢ (𝜑 → ◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺)) |
99 | | imacnvcnv 5517 |
. . . . 5
⊢ (◡◡𝐺 “ 𝑤) = (𝐺 “ 𝑤) |
100 | | fnwe.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) |
101 | | vex 3176 |
. . . . . . 7
⊢ 𝑤 ∈ V |
102 | | xpexg 6858 |
. . . . . . 7
⊢ (((𝐹 “ 𝑤) ∈ V ∧ 𝑤 ∈ V) → ((𝐹 “ 𝑤) × 𝑤) ∈ V) |
103 | 100, 101,
102 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((𝐹 “ 𝑤) × 𝑤) ∈ V) |
104 | | imadmres 5544 |
. . . . . . 7
⊢ (𝐺 “ dom (𝐺 ↾ 𝑤)) = (𝐺 “ 𝑤) |
105 | | dmres 5339 |
. . . . . . . . . . 11
⊢ dom
(𝐺 ↾ 𝑤) = (𝑤 ∩ dom 𝐺) |
106 | 105 | elin2 3763 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom (𝐺 ↾ 𝑤) ↔ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) |
107 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom 𝐺) |
108 | | f1dm 6018 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → dom 𝐺 = 𝐴) |
109 | 1, 36, 108 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐺 = 𝐴) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom 𝐺 = 𝐴) |
111 | 107, 110 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ 𝐴) |
112 | 111, 21 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐺‘𝑥) = 〈(𝐹‘𝑥), 𝑥〉) |
113 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
114 | 1, 113 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐴) |
115 | 114 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝐹 Fn 𝐴) |
116 | | dmres 5339 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹 ↾ 𝑤) = (𝑤 ∩ dom 𝐹) |
117 | | inss2 3796 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∩ dom 𝐹) ⊆ dom 𝐹 |
118 | | fndm 5904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom 𝐹 = 𝐴) |
120 | 117, 119 | syl5sseq 3616 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝑤 ∩ dom 𝐹) ⊆ 𝐴) |
121 | 116, 120 | syl5eqss 3612 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom (𝐹 ↾ 𝑤) ⊆ 𝐴) |
122 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ 𝑤) |
123 | 111, 119 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom 𝐹) |
124 | 116 | elin2 3763 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝑤) ↔ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐹)) |
125 | 122, 123,
124 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom (𝐹 ↾ 𝑤)) |
126 | | fnfvima 6400 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ dom (𝐹 ↾ 𝑤) ⊆ 𝐴 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝑤)) → (𝐹‘𝑥) ∈ (𝐹 “ dom (𝐹 ↾ 𝑤))) |
127 | 115, 121,
125, 126 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐹‘𝑥) ∈ (𝐹 “ dom (𝐹 ↾ 𝑤))) |
128 | | imadmres 5544 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ dom (𝐹 ↾ 𝑤)) = (𝐹 “ 𝑤) |
129 | 127, 128 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑤)) |
130 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) ∈ (𝐹 “ 𝑤) ∧ 𝑥 ∈ 𝑤) → 〈(𝐹‘𝑥), 𝑥〉 ∈ ((𝐹 “ 𝑤) × 𝑤)) |
131 | 129, 122,
130 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 〈(𝐹‘𝑥), 𝑥〉 ∈ ((𝐹 “ 𝑤) × 𝑤)) |
132 | 112, 131 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤)) |
133 | 106, 132 | sylan2b 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐺 ↾ 𝑤)) → (𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤)) |
134 | 133 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤)) |
135 | | f1fun 6016 |
. . . . . . . . . 10
⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → Fun 𝐺) |
136 | 1, 36, 135 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐺) |
137 | | resss 5342 |
. . . . . . . . . 10
⊢ (𝐺 ↾ 𝑤) ⊆ 𝐺 |
138 | | dmss 5245 |
. . . . . . . . . 10
⊢ ((𝐺 ↾ 𝑤) ⊆ 𝐺 → dom (𝐺 ↾ 𝑤) ⊆ dom 𝐺) |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
(𝐺 ↾ 𝑤) ⊆ dom 𝐺 |
140 | | funimass4 6157 |
. . . . . . . . 9
⊢ ((Fun
𝐺 ∧ dom (𝐺 ↾ 𝑤) ⊆ dom 𝐺) → ((𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤) ↔ ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤))) |
141 | 136, 139,
140 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤) ↔ ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤))) |
142 | 134, 141 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤)) |
143 | 104, 142 | syl5eqssr 3613 |
. . . . . 6
⊢ (𝜑 → (𝐺 “ 𝑤) ⊆ ((𝐹 “ 𝑤) × 𝑤)) |
144 | 103, 143 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → (𝐺 “ 𝑤) ∈ V) |
145 | 99, 144 | syl5eqel 2692 |
. . . 4
⊢ (𝜑 → (◡◡𝐺 “ 𝑤) ∈ V) |
146 | 145 | alrimiv 1842 |
. . 3
⊢ (𝜑 → ∀𝑤(◡◡𝐺 “ 𝑤) ∈ V) |
147 | | isowe2 6500 |
. . 3
⊢ ((◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺) ∧ ∀𝑤(◡◡𝐺 “ 𝑤) ∈ V) → (𝑄 We ran 𝐺 → 𝑇 We 𝐴)) |
148 | 98, 146, 147 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑄 We ran 𝐺 → 𝑇 We 𝐴)) |
149 | 16, 148 | mpd 15 |
1
⊢ (𝜑 → 𝑇 We 𝐴) |