Step | Hyp | Ref
| Expression |
1 | | funrel 6397 |
. . . . 5
⊢ (Fun
𝑓 → Rel 𝑓) |
2 | 1 | adantr 484 |
. . . 4
⊢ ((Fun
𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel 𝑓) |
3 | 2 | ralimi 3083 |
. . 3
⊢
(∀𝑓 ∈
𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 Rel 𝑓) |
4 | | reluni 5688 |
. . 3
⊢ (Rel
∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓) |
5 | 3, 4 | sylibr 237 |
. 2
⊢
(∀𝑓 ∈
𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Rel ∪
𝐴) |
6 | | r19.28v 3108 |
. . . 4
⊢ ((Fun
𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) |
7 | 6 | ralimi 3083 |
. . 3
⊢
(∀𝑓 ∈
𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) |
8 | | ssel 3893 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ 𝑣 → (〈𝑥, 𝑦〉 ∈ 𝑤 → 〈𝑥, 𝑦〉 ∈ 𝑣)) |
9 | 8 | anim1d 614 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ 𝑣 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → (〈𝑥, 𝑦〉 ∈ 𝑣 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣))) |
10 | | dffun4 6392 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝑣 ↔ (Rel 𝑣 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑣 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
11 | 10 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑣 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑣 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
12 | 11 | 19.21bbi 2187 |
. . . . . . . . . . . 12
⊢ (Fun
𝑣 → ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑣 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
13 | 12 | 19.21bi 2186 |
. . . . . . . . . . 11
⊢ (Fun
𝑣 → ((〈𝑥, 𝑦〉 ∈ 𝑣 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
14 | 9, 13 | syl9r 78 |
. . . . . . . . . 10
⊢ (Fun
𝑣 → (𝑤 ⊆ 𝑣 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
15 | 14 | adantl 485 |
. . . . . . . . 9
⊢ ((Fun
𝑤 ∧ Fun 𝑣) → (𝑤 ⊆ 𝑣 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
16 | | ssel 3893 |
. . . . . . . . . . . 12
⊢ (𝑣 ⊆ 𝑤 → (〈𝑥, 𝑧〉 ∈ 𝑣 → 〈𝑥, 𝑧〉 ∈ 𝑤)) |
17 | 16 | anim2d 615 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ 𝑤 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑤))) |
18 | | dffun4 6392 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝑤 ↔ (Rel 𝑤 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑤) → 𝑦 = 𝑧))) |
19 | 18 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑤 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑤) → 𝑦 = 𝑧)) |
20 | 19 | 19.21bbi 2187 |
. . . . . . . . . . . 12
⊢ (Fun
𝑤 → ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑤) → 𝑦 = 𝑧)) |
21 | 20 | 19.21bi 2186 |
. . . . . . . . . . 11
⊢ (Fun
𝑤 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑤) → 𝑦 = 𝑧)) |
22 | 17, 21 | syl9r 78 |
. . . . . . . . . 10
⊢ (Fun
𝑤 → (𝑣 ⊆ 𝑤 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
23 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((Fun
𝑤 ∧ Fun 𝑣) → (𝑣 ⊆ 𝑤 → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
24 | 15, 23 | jaod 859 |
. . . . . . . 8
⊢ ((Fun
𝑤 ∧ Fun 𝑣) → ((𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤) → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
25 | 24 | imp 410 |
. . . . . . 7
⊢ (((Fun
𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
26 | 25 | 2ralimi 3084 |
. . . . . 6
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) → ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
27 | | funeq 6400 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑤 → (Fun 𝑓 ↔ Fun 𝑤)) |
28 | | sseq1 3926 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑔)) |
29 | | sseq2 3927 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑔 ⊆ 𝑤)) |
30 | 28, 29 | orbi12d 919 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤))) |
31 | 27, 30 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑓 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)))) |
32 | | sseq2 3927 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → (𝑤 ⊆ 𝑔 ↔ 𝑤 ⊆ 𝑣)) |
33 | | sseq1 3926 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → (𝑔 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤)) |
34 | 32, 33 | orbi12d 919 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑣 → ((𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
35 | 34 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑔 = 𝑣 → ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑤)) ↔ (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
36 | 31, 35 | cbvral2vw 3371 |
. . . . . . . 8
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
37 | | ralcom 3267 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑔 ∈ 𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) |
38 | | orcom 870 |
. . . . . . . . . . . 12
⊢ ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔)) |
39 | | sseq1 3926 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑤 → (𝑔 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑓)) |
40 | | sseq2 3927 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑤 → (𝑓 ⊆ 𝑔 ↔ 𝑓 ⊆ 𝑤)) |
41 | 39, 40 | orbi12d 919 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑤 → ((𝑔 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑔) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤))) |
42 | 38, 41 | syl5bb 286 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑤 → ((𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓) ↔ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤))) |
43 | 42 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑤 → ((Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ (Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)))) |
44 | | funeq 6400 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑣 → (Fun 𝑓 ↔ Fun 𝑣)) |
45 | | sseq2 3927 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑣 → (𝑤 ⊆ 𝑓 ↔ 𝑤 ⊆ 𝑣)) |
46 | | sseq1 3926 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑣 → (𝑓 ⊆ 𝑤 ↔ 𝑣 ⊆ 𝑤)) |
47 | 45, 46 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑣 → ((𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤) ↔ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
48 | 44, 47 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑣 → ((Fun 𝑓 ∧ (𝑤 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑤)) ↔ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
49 | 43, 48 | cbvral2vw 3371 |
. . . . . . . . 9
⊢
(∀𝑔 ∈
𝐴 ∀𝑓 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
50 | 37, 49 | bitri 278 |
. . . . . . . 8
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
51 | 36, 50 | anbi12i 630 |
. . . . . . 7
⊢
((∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
52 | | anidm 568 |
. . . . . . 7
⊢
((∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) ↔ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓))) |
53 | | anandir 677 |
. . . . . . . . 9
⊢ (((Fun
𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
54 | 53 | 2ralbii 3089 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
55 | | r19.26-2 3093 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ (∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)))) |
56 | 54, 55 | bitr2i 279 |
. . . . . . 7
⊢
((∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑤 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤)) ∧ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (Fun 𝑣 ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
57 | 51, 52, 56 | 3bitr3i 304 |
. . . . . 6
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((Fun 𝑤 ∧ Fun 𝑣) ∧ (𝑤 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑤))) |
58 | | eluni 4822 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝐴
↔ ∃𝑤(〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴)) |
59 | | eluni 4822 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝐴
↔ ∃𝑣(〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) |
60 | 58, 59 | anbi12i 630 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ ∪ 𝐴
∧ 〈𝑥, 𝑧〉 ∈ ∪ 𝐴)
↔ (∃𝑤(〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴))) |
61 | | exdistrv 1964 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ (∃𝑤(〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ ∃𝑣(〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴))) |
62 | | an4 656 |
. . . . . . . . . . 11
⊢
(((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) ∧ (𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴))) |
63 | 62 | biancomi 466 |
. . . . . . . . . 10
⊢
(((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣))) |
64 | 63 | 2exbii 1856 |
. . . . . . . . 9
⊢
(∃𝑤∃𝑣((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴) ∧ (〈𝑥, 𝑧〉 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴)) ↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣))) |
65 | 60, 61, 64 | 3bitr2i 302 |
. . . . . . . 8
⊢
((〈𝑥, 𝑦〉 ∈ ∪ 𝐴
∧ 〈𝑥, 𝑧〉 ∈ ∪ 𝐴)
↔ ∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣))) |
66 | 65 | imbi1i 353 |
. . . . . . 7
⊢
(((〈𝑥, 𝑦〉 ∈ ∪ 𝐴
∧ 〈𝑥, 𝑧〉 ∈ ∪ 𝐴)
→ 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧)) |
67 | | 19.23v 1950 |
. . . . . . 7
⊢
(∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑤∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧)) |
68 | | r2al 3122 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝐴 ∀𝑣 ∈ 𝐴 ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
69 | | impexp 454 |
. . . . . . . . 9
⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
70 | 69 | 2albii 1828 |
. . . . . . . 8
⊢
(∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤∀𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧))) |
71 | | 19.23v 1950 |
. . . . . . . . 9
⊢
(∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ (∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧)) |
72 | 71 | albii 1827 |
. . . . . . . 8
⊢
(∀𝑤∀𝑣(((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧)) |
73 | 68, 70, 72 | 3bitr2ri 303 |
. . . . . . 7
⊢
(∀𝑤(∃𝑣((𝑤 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣)) → 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
74 | 66, 67, 73 | 3bitr2i 302 |
. . . . . 6
⊢
(((〈𝑥, 𝑦〉 ∈ ∪ 𝐴
∧ 〈𝑥, 𝑧〉 ∈ ∪ 𝐴)
→ 𝑦 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ((〈𝑥, 𝑦〉 ∈ 𝑤 ∧ 〈𝑥, 𝑧〉 ∈ 𝑣) → 𝑦 = 𝑧)) |
75 | 26, 57, 74 | 3imtr4i 295 |
. . . . 5
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
76 | 75 | alrimiv 1935 |
. . . 4
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
77 | 76 | alrimivv 1936 |
. . 3
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (Fun 𝑓 ∧ (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
78 | 7, 77 | syl 17 |
. 2
⊢
(∀𝑓 ∈
𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧)) |
79 | | dffun4 6392 |
. 2
⊢ (Fun
∪ 𝐴 ↔ (Rel ∪
𝐴 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ ∪
𝐴 ∧ 〈𝑥, 𝑧〉 ∈ ∪
𝐴) → 𝑦 = 𝑧))) |
80 | 5, 78, 79 | sylanbrc 586 |
1
⊢
(∀𝑓 ∈
𝐴 (Fun 𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ∪
𝐴) |