Proof of Theorem ofpreima2
Step | Hyp | Ref
| Expression |
1 | | ofpreima.1 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
2 | | ofpreima.2 |
. . . 4
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
3 | | ofpreima.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | | ofpreima.4 |
. . . 4
⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) |
5 | 1, 2, 3, 4 | ofpreima 30577 |
. . 3
⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
6 | | inundif 4368 |
. . . . 5
⊢ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) = (◡𝑅 “ 𝐷) |
7 | | iuneq1 4897 |
. . . . 5
⊢ ((((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) = (◡𝑅 “ 𝐷) → ∪
𝑝 ∈ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
8 | 6, 7 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑝 ∈ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) |
9 | | iunxun 4979 |
. . . 4
⊢ ∪ 𝑝 ∈ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
10 | 8, 9 | eqtr3i 2763 |
. . 3
⊢ ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
11 | 5, 10 | eqtrdi 2789 |
. 2
⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = (∪
𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
12 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) |
13 | 12 | eldifbd 3856 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ¬ 𝑝 ∈ (ran 𝐹 × ran 𝐺)) |
14 | | cnvimass 5923 |
. . . . . . . . . . . . . 14
⊢ (◡𝑅 “ 𝐷) ⊆ dom 𝑅 |
15 | 4 | fndmd 6442 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑅 = (𝐵 × 𝐶)) |
16 | 14, 15 | sseqtrid 3929 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑅 “ 𝐷) ⊆ (𝐵 × 𝐶)) |
17 | 16 | ssdifssd 4033 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)) ⊆ (𝐵 × 𝐶)) |
18 | 17 | sselda 3877 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐶)) |
19 | | 1st2nd2 7753 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (𝐵 × 𝐶) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
20 | | elxp6 7748 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) ↔ (𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∧ ((1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺))) |
21 | 20 | simplbi2 504 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉 →
(((1st ‘𝑝)
∈ ran 𝐹 ∧
(2nd ‘𝑝)
∈ ran 𝐺) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))) |
22 | 18, 19, 21 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (((1st ‘𝑝) ∈ ran 𝐹 ∧ (2nd ‘𝑝) ∈ ran 𝐺) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))) |
23 | 13, 22 | mtod 201 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ¬ ((1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺)) |
24 | | ianor 981 |
. . . . . . . . 9
⊢ (¬
((1st ‘𝑝)
∈ ran 𝐹 ∧
(2nd ‘𝑝)
∈ ran 𝐺) ↔ (¬
(1st ‘𝑝)
∈ ran 𝐹 ∨ ¬
(2nd ‘𝑝)
∈ ran 𝐺)) |
25 | 23, 24 | sylib 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (¬ (1st
‘𝑝) ∈ ran 𝐹 ∨ ¬ (2nd
‘𝑝) ∈ ran 𝐺)) |
26 | | disjsn 4602 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∩ {(1st
‘𝑝)}) = ∅
↔ ¬ (1st ‘𝑝) ∈ ran 𝐹) |
27 | | disjsn 4602 |
. . . . . . . . 9
⊢ ((ran
𝐺 ∩ {(2nd
‘𝑝)}) = ∅
↔ ¬ (2nd ‘𝑝) ∈ ran 𝐺) |
28 | 26, 27 | orbi12i 914 |
. . . . . . . 8
⊢ (((ran
𝐹 ∩ {(1st
‘𝑝)}) = ∅ ∨
(ran 𝐺 ∩
{(2nd ‘𝑝)}) = ∅) ↔ (¬ (1st
‘𝑝) ∈ ran 𝐹 ∨ ¬ (2nd
‘𝑝) ∈ ran 𝐺)) |
29 | 25, 28 | sylibr 237 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) =
∅)) |
30 | 1 | ffnd 6505 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐴) |
31 | | dffn3 6517 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
32 | 30, 31 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹) |
33 | 2 | ffnd 6505 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn 𝐴) |
34 | | dffn3 6517 |
. . . . . . . . . 10
⊢ (𝐺 Fn 𝐴 ↔ 𝐺:𝐴⟶ran 𝐺) |
35 | 33, 34 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐴⟶ran 𝐺) |
36 | 35 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝐺:𝐴⟶ran 𝐺) |
37 | | fimacnvdisj 6556 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ (ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅) → (◡𝐹 “ {(1st ‘𝑝)}) = ∅) |
38 | | ineq1 4096 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∅ ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
39 | | 0in 4282 |
. . . . . . . . . . . 12
⊢ (∅
∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅ |
40 | 38, 39 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
41 | 37, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ (ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
42 | 41 | ex 416 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ran 𝐹 → ((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
43 | | fimacnvdisj 6556 |
. . . . . . . . . . 11
⊢ ((𝐺:𝐴⟶ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅) → (◡𝐺 “ {(2nd ‘𝑝)}) = ∅) |
44 | | ineq2 4097 |
. . . . . . . . . . . 12
⊢ ((◡𝐺 “ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ((◡𝐹 “ {(1st ‘𝑝)}) ∩
∅)) |
45 | | in0 4280 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ ∅) =
∅ |
46 | 44, 45 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
47 | 43, 46 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺:𝐴⟶ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
48 | 47 | ex 416 |
. . . . . . . . 9
⊢ (𝐺:𝐴⟶ran 𝐺 → ((ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
49 | 42, 48 | jaao 954 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝐺:𝐴⟶ran 𝐺) → (((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) = ∅)
→ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
50 | 32, 36, 49 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) = ∅)
→ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
51 | 29, 50 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
52 | 51 | iuneq2dv 4905 |
. . . . 5
⊢ (𝜑 → ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))∅) |
53 | | iun0 4947 |
. . . . 5
⊢ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))∅ = ∅ |
54 | 52, 53 | eqtrdi 2789 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
55 | 54 | uneq2d 4053 |
. . 3
⊢ (𝜑 → (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪
∅)) |
56 | | un0 4279 |
. . 3
⊢ (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∅) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) |
57 | 55, 56 | eqtrdi 2789 |
. 2
⊢ (𝜑 → (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
58 | 11, 57 | eqtrd 2773 |
1
⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪
𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |