Proof of Theorem bnj1379
Step | Hyp | Ref
| Expression |
1 | | bnj1379.3 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) |
2 | | bnj1379.1 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) |
3 | 2 | bnj1095 32474 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓𝜑) |
4 | 3 | nf5i 2146 |
. . . . . 6
⊢
Ⅎ𝑓𝜑 |
5 | | nfra1 3140 |
. . . . . 6
⊢
Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
6 | 4, 5 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
7 | 1, 6 | nfxfr 1860 |
. . . 4
⊢
Ⅎ𝑓𝜓 |
8 | 2 | bnj946 32467 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
9 | 8 | biimpi 219 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
10 | 9 | 19.21bi 2186 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
11 | 1, 10 | bnj832 32450 |
. . . . 5
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
12 | | funrel 6397 |
. . . . 5
⊢ (Fun
𝑓 → Rel 𝑓) |
13 | 11, 12 | syl6 35 |
. . . 4
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓)) |
14 | 7, 13 | ralrimi 3137 |
. . 3
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓) |
15 | | reluni 5688 |
. . 3
⊢ (Rel
∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓) |
16 | 14, 15 | sylibr 237 |
. 2
⊢ (𝜓 → Rel ∪ 𝐴) |
17 | | bnj1379.5 |
. . . . . 6
⊢ (𝜒 ↔ (𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴)) |
18 | | eluni2 4823 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
↔ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
19 | 18 | biimpi 219 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
20 | 19 | bnj1196 32487 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
21 | 17, 20 | bnj836 32452 |
. . . . . . . . 9
⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
22 | | bnj1379.6 |
. . . . . . . . 9
⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
23 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
24 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
25 | 7, 23, 24 | nf3an 1909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑓(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
26 | 17, 25 | nfxfr 1860 |
. . . . . . . . . 10
⊢
Ⅎ𝑓𝜒 |
27 | 26 | nf5ri 2193 |
. . . . . . . . 9
⊢ (𝜒 → ∀𝑓𝜒) |
28 | 21, 22, 27 | bnj1345 32517 |
. . . . . . . 8
⊢ (𝜒 → ∃𝑓𝜃) |
29 | 17 | simp3bi 1149 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
30 | 22, 29 | bnj835 32451 |
. . . . . . . . . . . 12
⊢ (𝜃 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
31 | | eluni2 4823 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
32 | 31 | biimpi 219 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
33 | 32 | bnj1196 32487 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
35 | | bnj1379.7 |
. . . . . . . . . . 11
⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
36 | | nfv 1922 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔𝜑 |
37 | | nfra2w 3149 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
38 | 36, 37 | nfan 1907 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
39 | 1, 38 | nfxfr 1860 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔𝜓 |
40 | | nfv 1922 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
41 | | nfv 1922 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
42 | 39, 40, 41 | nf3an 1909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑔(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
43 | 17, 42 | nfxfr 1860 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔𝜒 |
44 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔 𝑓 ∈ 𝐴 |
45 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ 𝑓 |
46 | 43, 44, 45 | nf3an 1909 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓) |
47 | 22, 46 | nfxfr 1860 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑔𝜃 |
48 | 47 | nf5ri 2193 |
. . . . . . . . . . 11
⊢ (𝜃 → ∀𝑔𝜃) |
49 | 34, 35, 48 | bnj1345 32517 |
. . . . . . . . . 10
⊢ (𝜃 → ∃𝑔𝜏) |
50 | 1 | simprbi 500 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
51 | 17, 50 | bnj835 32451 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
52 | 22, 51 | bnj835 32451 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
53 | 35, 52 | bnj835 32451 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
54 | 22, 35 | bnj1219 32493 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑓 ∈ 𝐴) |
55 | 53, 54 | bnj1294 32510 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
56 | 35 | simp2bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑔 ∈ 𝐴) |
57 | 55, 56 | bnj1294 32510 |
. . . . . . . . . . . . 13
⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
58 | 57 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥)) |
59 | 22 | simp3bi 1149 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
60 | 35, 59 | bnj835 32451 |
. . . . . . . . . . . . . . . 16
⊢ (𝜏 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
61 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
62 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
63 | 61, 62 | opeldm 5776 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑓 → 𝑥 ∈ dom 𝑓) |
64 | 60, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑓) |
65 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
66 | 61, 65 | opeldm 5776 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑧〉 ∈ 𝑔 → 𝑥 ∈ dom 𝑔) |
67 | 35, 66 | bnj837 32453 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑔) |
68 | 64, 67 | elind 4108 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)) |
69 | | bnj1379.2 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) |
70 | 68, 69 | eleqtrrdi 2849 |
. . . . . . . . . . . . 13
⊢ (𝜏 → 𝑥 ∈ 𝐷) |
71 | 70 | fvresd 6737 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥)) |
72 | 70 | fvresd 6737 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥)) |
73 | 58, 71, 72 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
74 | 2 | biimpi 219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
75 | 1, 74 | bnj832 32450 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
76 | 17, 75 | bnj835 32451 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
77 | 22, 76 | bnj835 32451 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
78 | 35, 77 | bnj835 32451 |
. . . . . . . . . . . . 13
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
79 | 78, 54 | bnj1294 32510 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑓) |
80 | | funopfv 6764 |
. . . . . . . . . . . 12
⊢ (Fun
𝑓 → (〈𝑥, 𝑦〉 ∈ 𝑓 → (𝑓‘𝑥) = 𝑦)) |
81 | 79, 60, 80 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = 𝑦) |
82 | | funeq 6400 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔)) |
83 | 82, 78, 56 | rspcdva 3539 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑔) |
84 | 35 | simp3bi 1149 |
. . . . . . . . . . . 12
⊢ (𝜏 → 〈𝑥, 𝑧〉 ∈ 𝑔) |
85 | | funopfv 6764 |
. . . . . . . . . . . 12
⊢ (Fun
𝑔 → (〈𝑥, 𝑧〉 ∈ 𝑔 → (𝑔‘𝑥) = 𝑧)) |
86 | 83, 84, 85 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑔‘𝑥) = 𝑧) |
87 | 73, 81, 86 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜏 → 𝑦 = 𝑧) |
88 | 49, 87 | bnj593 32437 |
. . . . . . . . 9
⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧) |
89 | 88 | bnj937 32464 |
. . . . . . . 8
⊢ (𝜃 → 𝑦 = 𝑧) |
90 | 28, 89 | bnj593 32437 |
. . . . . . 7
⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧) |
91 | 90 | bnj937 32464 |
. . . . . 6
⊢ (𝜒 → 𝑦 = 𝑧) |
92 | 17, 91 | sylbir 238 |
. . . . 5
⊢ ((𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧) |
93 | 92 | 3expib 1124 |
. . . 4
⊢ (𝜓 → ((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
94 | 93 | alrimivv 1936 |
. . 3
⊢ (𝜓 → ∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
95 | 94 | alrimiv 1935 |
. 2
⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
96 | | dffun4 6392 |
. 2
⊢ (Fun
∪ 𝐴 ↔ (Rel ∪
𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧))) |
97 | 16, 95, 96 | sylanbrc 586 |
1
⊢ (𝜓 → Fun ∪ 𝐴) |