Proof of Theorem bnj1379
| Step | Hyp | Ref
| Expression |
| 1 | | bnj1379.3 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) |
| 2 | | bnj1379.1 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 3 | 2 | bnj1095 34795 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓𝜑) |
| 4 | 3 | nf5i 2146 |
. . . . . 6
⊢
Ⅎ𝑓𝜑 |
| 5 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
| 6 | 4, 5 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 7 | 1, 6 | nfxfr 1853 |
. . . 4
⊢
Ⅎ𝑓𝜓 |
| 8 | 2 | bnj946 34788 |
. . . . . . . 8
⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
| 9 | 8 | biimpi 216 |
. . . . . . 7
⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
| 10 | 9 | 19.21bi 2189 |
. . . . . 6
⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
| 11 | 1, 10 | bnj832 34772 |
. . . . 5
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓)) |
| 12 | | funrel 6583 |
. . . . 5
⊢ (Fun
𝑓 → Rel 𝑓) |
| 13 | 11, 12 | syl6 35 |
. . . 4
⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓)) |
| 14 | 7, 13 | ralrimi 3257 |
. . 3
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓) |
| 15 | | reluni 5828 |
. . 3
⊢ (Rel
∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓) |
| 16 | 14, 15 | sylibr 234 |
. 2
⊢ (𝜓 → Rel ∪ 𝐴) |
| 17 | | bnj1379.5 |
. . . . . 6
⊢ (𝜒 ↔ (𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴)) |
| 18 | | eluni2 4911 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
↔ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
| 19 | 18 | biimpi 216 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓 ∈
𝐴 〈𝑥, 𝑦〉 ∈ 𝑓) |
| 20 | 19 | bnj1196 34808 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
→ ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
| 21 | 17, 20 | bnj836 34774 |
. . . . . . . . 9
⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
| 22 | | bnj1379.6 |
. . . . . . . . 9
⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓)) |
| 23 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
| 24 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑓〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
| 25 | 7, 23, 24 | nf3an 1901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑓(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
| 26 | 17, 25 | nfxfr 1853 |
. . . . . . . . . 10
⊢
Ⅎ𝑓𝜒 |
| 27 | 26 | nf5ri 2195 |
. . . . . . . . 9
⊢ (𝜒 → ∀𝑓𝜒) |
| 28 | 21, 22, 27 | bnj1345 34838 |
. . . . . . . 8
⊢ (𝜒 → ∃𝑓𝜃) |
| 29 | 17 | simp3bi 1148 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
| 30 | 22, 29 | bnj835 34773 |
. . . . . . . . . . . 12
⊢ (𝜃 → 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
| 31 | | eluni2 4911 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
| 32 | 31 | biimpi 216 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔 ∈
𝐴 〈𝑥, 𝑧〉 ∈ 𝑔) |
| 33 | 32 | bnj1196 34808 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
→ ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
| 34 | 30, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
| 35 | | bnj1379.7 |
. . . . . . . . . . 11
⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ 〈𝑥, 𝑧〉 ∈ 𝑔)) |
| 36 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔𝜑 |
| 37 | | nfra2w 3299 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) |
| 38 | 36, 37 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 39 | 1, 38 | nfxfr 1853 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔𝜓 |
| 40 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ ∪
𝐴 |
| 41 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑔〈𝑥, 𝑧〉 ∈ ∪
𝐴 |
| 42 | 39, 40, 41 | nf3an 1901 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑔(𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) |
| 43 | 17, 42 | nfxfr 1853 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔𝜒 |
| 44 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔 𝑓 ∈ 𝐴 |
| 45 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑔〈𝑥, 𝑦〉 ∈ 𝑓 |
| 46 | 43, 44, 45 | nf3an 1901 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝑓) |
| 47 | 22, 46 | nfxfr 1853 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑔𝜃 |
| 48 | 47 | nf5ri 2195 |
. . . . . . . . . . 11
⊢ (𝜃 → ∀𝑔𝜃) |
| 49 | 34, 35, 48 | bnj1345 34838 |
. . . . . . . . . 10
⊢ (𝜃 → ∃𝑔𝜏) |
| 50 | 1 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 51 | 17, 50 | bnj835 34773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 52 | 22, 51 | bnj835 34773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 53 | 35, 52 | bnj835 34773 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 54 | 22, 35 | bnj1219 34814 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑓 ∈ 𝐴) |
| 55 | 53, 54 | bnj1294 34831 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 56 | 35 | simp2bi 1147 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑔 ∈ 𝐴) |
| 57 | 55, 56 | bnj1294 34831 |
. . . . . . . . . . . . 13
⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 58 | 57 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥)) |
| 59 | 22 | simp3bi 1148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
| 60 | 35, 59 | bnj835 34773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜏 → 〈𝑥, 𝑦〉 ∈ 𝑓) |
| 61 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
| 62 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
| 63 | 61, 62 | opeldm 5918 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝑓 → 𝑥 ∈ dom 𝑓) |
| 64 | 60, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑓) |
| 65 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
| 66 | 61, 65 | opeldm 5918 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑧〉 ∈ 𝑔 → 𝑥 ∈ dom 𝑔) |
| 67 | 35, 66 | bnj837 34775 |
. . . . . . . . . . . . . . 15
⊢ (𝜏 → 𝑥 ∈ dom 𝑔) |
| 68 | 64, 67 | elind 4200 |
. . . . . . . . . . . . . 14
⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)) |
| 69 | | bnj1379.2 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) |
| 70 | 68, 69 | eleqtrrdi 2852 |
. . . . . . . . . . . . 13
⊢ (𝜏 → 𝑥 ∈ 𝐷) |
| 71 | 70 | fvresd 6926 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥)) |
| 72 | 70 | fvresd 6926 |
. . . . . . . . . . . 12
⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥)) |
| 73 | 58, 71, 72 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
| 74 | 2 | biimpi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 75 | 1, 74 | bnj832 34772 |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 76 | 17, 75 | bnj835 34773 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 77 | 22, 76 | bnj835 34773 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 78 | 35, 77 | bnj835 34773 |
. . . . . . . . . . . . 13
⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 79 | 78, 54 | bnj1294 34831 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑓) |
| 80 | | funopfv 6958 |
. . . . . . . . . . . 12
⊢ (Fun
𝑓 → (〈𝑥, 𝑦〉 ∈ 𝑓 → (𝑓‘𝑥) = 𝑦)) |
| 81 | 79, 60, 80 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑓‘𝑥) = 𝑦) |
| 82 | | funeq 6586 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔)) |
| 83 | 82, 78, 56 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ (𝜏 → Fun 𝑔) |
| 84 | 35 | simp3bi 1148 |
. . . . . . . . . . . 12
⊢ (𝜏 → 〈𝑥, 𝑧〉 ∈ 𝑔) |
| 85 | | funopfv 6958 |
. . . . . . . . . . . 12
⊢ (Fun
𝑔 → (〈𝑥, 𝑧〉 ∈ 𝑔 → (𝑔‘𝑥) = 𝑧)) |
| 86 | 83, 84, 85 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜏 → (𝑔‘𝑥) = 𝑧) |
| 87 | 73, 81, 86 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜏 → 𝑦 = 𝑧) |
| 88 | 49, 87 | bnj593 34759 |
. . . . . . . . 9
⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧) |
| 89 | 88 | bnj937 34785 |
. . . . . . . 8
⊢ (𝜃 → 𝑦 = 𝑧) |
| 90 | 28, 89 | bnj593 34759 |
. . . . . . 7
⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧) |
| 91 | 90 | bnj937 34785 |
. . . . . 6
⊢ (𝜒 → 𝑦 = 𝑧) |
| 92 | 17, 91 | sylbir 235 |
. . . . 5
⊢ ((𝜓 ∧ 〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧) |
| 93 | 92 | 3expib 1123 |
. . . 4
⊢ (𝜓 → ((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
| 94 | 93 | alrimivv 1928 |
. . 3
⊢ (𝜓 → ∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
| 95 | 94 | alrimiv 1927 |
. 2
⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
| 96 | | dffun4 6577 |
. 2
⊢ (Fun
∪ 𝐴 ↔ (Rel ∪
𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧))) |
| 97 | 16, 95, 96 | sylanbrc 583 |
1
⊢ (𝜓 → Fun ∪ 𝐴) |