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 28848 |
. . 3
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
6 | | inundif 3998 |
. . . . 5
⊢ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) = (◡𝑅 “ 𝐷) |
7 | | iuneq1 4470 |
. . . . 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 4541 |
. . . 4
⊢ ∪ 𝑝 ∈ (((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺)) ∪ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
10 | 8, 9 | eqtr3i 2634 |
. . 3
⊢ ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
11 | 5, 10 | syl6eq 2660 |
. 2
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = (∪
𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
12 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) |
13 | 12 | eldifbd 3553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ¬ 𝑝 ∈ (ran 𝐹 × ran 𝐺)) |
14 | | cnvimass 5404 |
. . . . . . . . . . . . . 14
⊢ (◡𝑅 “ 𝐷) ⊆ dom 𝑅 |
15 | | fndm 5904 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Fn (𝐵 × 𝐶) → dom 𝑅 = (𝐵 × 𝐶)) |
16 | 4, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑅 = (𝐵 × 𝐶)) |
17 | 14, 16 | syl5sseq 3616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑅 “ 𝐷) ⊆ (𝐵 × 𝐶)) |
18 | 17 | ssdifssd 3710 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺)) ⊆ (𝐵 × 𝐶)) |
19 | 18 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐶)) |
20 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (𝐵 × 𝐶) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
21 | | elxp6 7091 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) ↔ (𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∧ ((1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺))) |
22 | 21 | simplbi2 653 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉 →
(((1st ‘𝑝)
∈ ran 𝐹 ∧
(2nd ‘𝑝)
∈ ran 𝐺) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))) |
23 | 19, 20, 22 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (((1st ‘𝑝) ∈ ran 𝐹 ∧ (2nd ‘𝑝) ∈ ran 𝐺) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))) |
24 | 13, 23 | mtod 188 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ¬ ((1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺)) |
25 | | ianor 508 |
. . . . . . . . 9
⊢ (¬
((1st ‘𝑝)
∈ ran 𝐹 ∧
(2nd ‘𝑝)
∈ ran 𝐺) ↔ (¬
(1st ‘𝑝)
∈ ran 𝐹 ∨ ¬
(2nd ‘𝑝)
∈ ran 𝐺)) |
26 | 24, 25 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (¬ (1st
‘𝑝) ∈ ran 𝐹 ∨ ¬ (2nd
‘𝑝) ∈ ran 𝐺)) |
27 | | disjsn 4192 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∩ {(1st
‘𝑝)}) = ∅
↔ ¬ (1st ‘𝑝) ∈ ran 𝐹) |
28 | | disjsn 4192 |
. . . . . . . . 9
⊢ ((ran
𝐺 ∩ {(2nd
‘𝑝)}) = ∅
↔ ¬ (2nd ‘𝑝) ∈ ran 𝐺) |
29 | 27, 28 | orbi12i 542 |
. . . . . . . 8
⊢ (((ran
𝐹 ∩ {(1st
‘𝑝)}) = ∅ ∨
(ran 𝐺 ∩
{(2nd ‘𝑝)}) = ∅) ↔ (¬ (1st
‘𝑝) ∈ ran 𝐹 ∨ ¬ (2nd
‘𝑝) ∈ ran 𝐺)) |
30 | 26, 29 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) =
∅)) |
31 | 1 | ffnd 5959 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐴) |
32 | | dffn3 5967 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
33 | 31, 32 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹) |
34 | 2 | ffnd 5959 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn 𝐴) |
35 | | dffn3 5967 |
. . . . . . . . . 10
⊢ (𝐺 Fn 𝐴 ↔ 𝐺:𝐴⟶ran 𝐺) |
36 | 34, 35 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐴⟶ran 𝐺) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → 𝐺:𝐴⟶ran 𝐺) |
38 | | fimacnvdisj 5996 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ (ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅) → (◡𝐹 “ {(1st ‘𝑝)}) = ∅) |
39 | | ineq1 3769 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = (∅ ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
40 | | 0in 3921 |
. . . . . . . . . . . 12
⊢ (∅
∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅ |
41 | 39, 40 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
42 | 38, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ (ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
43 | 42 | ex 449 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ran 𝐹 → ((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
44 | | fimacnvdisj 5996 |
. . . . . . . . . . 11
⊢ ((𝐺:𝐴⟶ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅) → (◡𝐺 “ {(2nd ‘𝑝)}) = ∅) |
45 | | ineq2 3770 |
. . . . . . . . . . . 12
⊢ ((◡𝐺 “ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ((◡𝐹 “ {(1st ‘𝑝)}) ∩
∅)) |
46 | | in0 3920 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ ∅) =
∅ |
47 | 45, 46 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
48 | 44, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐺:𝐴⟶ran 𝐺 ∧ (ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
49 | 48 | ex 449 |
. . . . . . . . 9
⊢ (𝐺:𝐴⟶ran 𝐺 → ((ran 𝐺 ∩ {(2nd ‘𝑝)}) = ∅ → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
50 | 43, 49 | jaao 530 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ran 𝐹 ∧ 𝐺:𝐴⟶ran 𝐺) → (((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) = ∅)
→ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
51 | 33, 37, 50 | syl2an2r 872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → (((ran 𝐹 ∩ {(1st ‘𝑝)}) = ∅ ∨ (ran 𝐺 ∩ {(2nd
‘𝑝)}) = ∅)
→ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) =
∅)) |
52 | 30, 51 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
53 | 52 | iuneq2dv 4478 |
. . . . 5
⊢ (𝜑 → ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))∅) |
54 | | iun0 4512 |
. . . . 5
⊢ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))∅ = ∅ |
55 | 53, 54 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) = ∅) |
56 | 55 | uneq2d 3729 |
. . 3
⊢ (𝜑 → (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪
∅)) |
57 | | un0 3919 |
. . 3
⊢ (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∅) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) |
58 | 56, 57 | syl6eq 2660 |
. 2
⊢ (𝜑 → (∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∪ ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∖ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
59 | 11, 58 | eqtrd 2644 |
1
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪
𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |