Proof of Theorem bnj1379
Step | Hyp | Ref
| Expression |
1 | | bnj1379.3 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) |
2 | | bnj1379.1 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) |
3 | 2 | bnj1095 30852 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓𝜑) |
4 | 3 | nf5i 2024 |
. . . . . 6
⊢
Ⅎ𝑓𝜑 |
5 | | nfra1 2941 |
. . . . . 6
⊢
Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
6 | 4, 5 | nfan 1828 |
. . . . 5
⊢
Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
7 | 1, 6 | nfxfr 1779 |
. . . 4
⊢
Ⅎ𝑓𝜓 |
8 | 2 | bnj946 30845 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
9 | 8 | biimpi 206 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
10 | 9 | 19.21bi 2059 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
11 | 1, 10 | bnj832 30828 |
. . . . 5
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
12 | | funrel 5905 |
. . . . 5
⊢ (Fun
𝑓 → Rel 𝑓) |
13 | 11, 12 | syl6 35 |
. . . 4
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓)) |
14 | 7, 13 | ralrimi 2957 |
. . 3
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓) |
15 | | reluni 5241 |
. . 3
⊢ (Rel
∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓) |
16 | 14, 15 | sylibr 224 |
. 2
⊢ (𝜓 → Rel ∪ 𝐴) |
17 | | bnj1379.5 |
. . . . . 6
⊢ (𝜒 ↔ (𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴)) |
18 | | eluni2 4440 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
↔ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
19 | 18 | biimpi 206 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
20 | 19 | bnj1196 30865 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
21 | 17, 20 | bnj836 30830 |
. . . . . . . . 9
⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
22 | | bnj1379.6 |
. . . . . . . . 9
⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
23 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
24 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
25 | 7, 23, 24 | nf3an 1831 |
. . . . . . . . . . 11
⊢
Ⅎ𝑓(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
26 | 17, 25 | nfxfr 1779 |
. . . . . . . . . 10
⊢
Ⅎ𝑓𝜒 |
27 | 26 | nf5ri 2065 |
. . . . . . . . 9
⊢ (𝜒 → ∀𝑓𝜒) |
28 | 21, 22, 27 | bnj1345 30895 |
. . . . . . . 8
⊢ (𝜒 → ∃𝑓𝜃) |
29 | 17 | simp3bi 1078 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
30 | 22, 29 | bnj835 30829 |
. . . . . . . . . . . 12
⊢ (𝜃 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
31 | | eluni2 4440 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
32 | 31 | biimpi 206 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
33 | 32 | bnj1196 30865 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
35 | | bnj1379.7 |
. . . . . . . . . . 11
⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
36 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔𝜑 |
37 | | nfra2 2946 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
38 | 36, 37 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
39 | 1, 38 | nfxfr 1779 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔𝜓 |
40 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
41 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
42 | 39, 40, 41 | nf3an 1831 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑔(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
43 | 17, 42 | nfxfr 1779 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔𝜒 |
44 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔 𝑓 ∈ 𝐴 |
45 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ 𝑓 |
46 | 43, 44, 45 | nf3an 1831 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓) |
47 | 22, 46 | nfxfr 1779 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑔𝜃 |
48 | 47 | nf5ri 2065 |
. . . . . . . . . . 11
⊢ (𝜃 → ∀𝑔𝜃) |
49 | 34, 35, 48 | bnj1345 30895 |
. . . . . . . . . 10
⊢ (𝜃 → ∃𝑔𝜏) |
50 | 1 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
51 | 17, 50 | bnj835 30829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
52 | 22, 51 | bnj835 30829 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
53 | 35, 52 | bnj835 30829 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
54 | 22, 35 | bnj1219 30871 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑓 ∈ 𝐴) |
55 | 53, 54 | bnj1294 30888 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
56 | 35 | simp2bi 1077 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑔 ∈ 𝐴) |
57 | 55, 56 | bnj1294 30888 |
. . . . . . . . . . . . 13
⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
58 | 57 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥)) |
59 | 22 | simp3bi 1078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
60 | 35, 59 | bnj835 30829 |
. . . . . . . . . . . . . . . 16
⊢ (𝜏 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
61 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
62 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
63 | 61, 62 | opeldm 5328 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑓 → 𝑥 ∈ dom 𝑓) |
64 | 60, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑓) |
65 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
66 | 61, 65 | opeldm 5328 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑧〉 ∈ 𝑔 → 𝑥 ∈ dom 𝑔) |
67 | 35, 66 | bnj837 30831 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑔) |
68 | 64, 67 | elind 3798 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)) |
69 | | bnj1379.2 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) |
70 | 68, 69 | syl6eleqr 2712 |
. . . . . . . . . . . . 13
⊢ (𝜏 → 𝑥 ∈ 𝐷) |
71 | | fvres 6207 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥)) |
73 | | fvres 6207 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥)) |
74 | 70, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥)) |
75 | 58, 72, 74 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
76 | 2 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
77 | 1, 76 | bnj832 30828 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
78 | 17, 77 | bnj835 30829 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
79 | 22, 78 | bnj835 30829 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
80 | 35, 79 | bnj835 30829 |
. . . . . . . . . . . . 13
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
81 | 80, 54 | bnj1294 30888 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑓) |
82 | | funopfv 6235 |
. . . . . . . . . . . 12
⊢ (Fun
𝑓 → (〈𝑥, 𝑦〉 ∈ 𝑓 → (𝑓‘𝑥) = 𝑦)) |
83 | 81, 60, 82 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = 𝑦) |
84 | | funeq 5908 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔)) |
85 | 84 | cbvralv 3171 |
. . . . . . . . . . . . . 14
⊢
(∀𝑓 ∈
𝐴 Fun 𝑓 ↔ ∀𝑔 ∈ 𝐴 Fun 𝑔) |
86 | 80, 85 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜏 → ∀𝑔 ∈ 𝐴 Fun 𝑔) |
87 | 86, 56 | bnj1294 30888 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑔) |
88 | 35 | simp3bi 1078 |
. . . . . . . . . . . 12
⊢ (𝜏 → 〈𝑥, 𝑧〉 ∈ 𝑔) |
89 | | funopfv 6235 |
. . . . . . . . . . . 12
⊢ (Fun
𝑔 → (〈𝑥, 𝑧〉 ∈ 𝑔 → (𝑔‘𝑥) = 𝑧)) |
90 | 87, 88, 89 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑔‘𝑥) = 𝑧) |
91 | 75, 83, 90 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ (𝜏 → 𝑦 = 𝑧) |
92 | 49, 91 | bnj593 30815 |
. . . . . . . . 9
⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧) |
93 | 92 | bnj937 30842 |
. . . . . . . 8
⊢ (𝜃 → 𝑦 = 𝑧) |
94 | 28, 93 | bnj593 30815 |
. . . . . . 7
⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧) |
95 | 94 | bnj937 30842 |
. . . . . 6
⊢ (𝜒 → 𝑦 = 𝑧) |
96 | 17, 95 | sylbir 225 |
. . . . 5
⊢ ((𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧) |
97 | 96 | 3expib 1268 |
. . . 4
⊢ (𝜓 → ((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
98 | 97 | alrimivv 1856 |
. . 3
⊢ (𝜓 → ∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
99 | 98 | alrimiv 1855 |
. 2
⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
100 | | dffun4 5900 |
. 2
⊢ (Fun
∪ 𝐴 ↔ (Rel ∪
𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧))) |
101 | 16, 99, 100 | sylanbrc 698 |
1
⊢ (𝜓 → Fun ∪ 𝐴) |