Step | Hyp | Ref
| Expression |
1 | | disjinfi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
2 | | id 22 |
. . . 4
⊢ (𝐶 ∈ Fin → 𝐶 ∈ Fin) |
3 | | inss2 3834 |
. . . . 5
⊢ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝐶 ∈ Fin → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
5 | | ssfi 8180 |
. . . 4
⊢ ((𝐶 ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) → (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
6 | 2, 4, 5 | syl2anc 693 |
. . 3
⊢ (𝐶 ∈ Fin → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
7 | 1, 6 | syl 17 |
. 2
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
8 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
9 | 8, 1 | jca 554 |
. . . 4
⊢ (𝜑 → ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin)) |
10 | | ssexg 4804 |
. . . 4
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin) → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
12 | | elinel1 3799 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
13 | | eluni2 4440 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
14 | 13 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
15 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
17 | 16 | elrnmpt 5372 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)) |
18 | 15, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
19 | 18 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
21 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑤 |
22 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
23 | 22 | nfrn 5368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
24 | 21, 23 | nfel 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
25 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑦 ∈ 𝑤 |
26 | 24, 25 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) |
27 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝑤) |
28 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑤 = 𝐵) |
29 | 27, 28 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝐵) |
30 | 29 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝑤 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)) |
31 | 30 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑤 → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
33 | 26, 32 | reximdai 3012 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
34 | 20, 33 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
35 | 34 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))) |
37 | 36 | rexlimdv 3030 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
38 | 14, 37 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
40 | 39 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
41 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜑 |
42 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑦 |
43 | 23 | nfuni 4442 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
44 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐶 |
45 | 43, 44 | nfin 3820 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
46 | 42, 45 | nfel 2777 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
47 | 41, 46 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
48 | | nfre1 3005 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) |
49 | 3 | sseli 3599 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ 𝐶) |
50 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
51 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
52 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐶) |
53 | 51, 52 | elind 3798 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
54 | 53 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
55 | | rspe 3003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
56 | 50, 54, 55 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
57 | 56 | 3exp 1264 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
58 | 49, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
59 | 58 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
60 | 47, 48, 59 | rexlimd 3026 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
61 | 40, 60 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
62 | | disjinfi.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
63 | | disjors 4635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
64 | 62, 63 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
65 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑧∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
66 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥𝐴 |
67 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑧 = 𝑤 |
68 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
69 | 21 | nfcsb1 3548 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
70 | 68, 69 | nfin 3820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) |
71 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥∅ |
72 | 70, 71 | nfeq 2776 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ |
73 | 67, 72 | nfor 1834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
74 | 66, 73 | nfral 2945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
75 | | equequ1 1952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
76 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
77 | 76 | ineq1d 3813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵)) |
78 | 77 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
79 | 75, 78 | orbi12d 746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
80 | 79 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
81 | 65, 74, 80 | cbvral 3167 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
82 | 64, 81 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
83 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
84 | 82, 83 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
86 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
87 | | rspa 2930 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
88 | 87 | orcomd 403 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
89 | 85, 86, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
91 | | elinel1 3799 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐵) |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐵) |
93 | | sbsbc 3439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
94 | | sbcel2 3989 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶)) |
95 | | csbin 4010 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋𝑤 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) |
96 | 95 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
97 | 93, 94, 96 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
98 | 97 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
99 | | elinel1 3799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
102 | 92, 101 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)) |
103 | | inelcm 4032 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) ≠ ∅) |
104 | 103 | neneqd 2799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
107 | | pm2.53 388 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ → 𝑥 = 𝑤)) |
108 | 90, 106, 107 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → 𝑥 = 𝑤) |
109 | 108 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
110 | 109 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
111 | 110 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
112 | 111 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
113 | 61, 112 | jca 554 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
114 | | reu2 3394 |
. . . . . . . . 9
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
115 | 113, 114 | sylibr 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
116 | | riotacl2 6624 |
. . . . . . . 8
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
117 | 115, 116 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
118 | | nfriota1 6618 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
119 | 118 | nfcsb1 3548 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 |
120 | 119, 44 | nfin 3820 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
121 | 42, 120 | nfel 2777 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑦 ∈
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
122 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝐵 = ⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵) |
123 | 122 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝐵 ∩ 𝐶) = (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
124 | 123 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
125 | 118, 66, 121, 124 | elrabf 3360 |
. . . . . . . . . . 11
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
126 | 125 | biimpi 206 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
127 | 126 | simpld 475 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴) |
128 | 126 | simprd 479 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
129 | | ne0i 3921 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) →
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
130 | 128, 129 | syl 17 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} →
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
131 | 127, 130 | jca 554 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
132 | 120, 71 | nfne 2894 |
. . . . . . . . 9
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
133 | 123 | neeq1d 2853 |
. . . . . . . . 9
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → ((𝐵 ∩ 𝐶) ≠ ∅ ↔
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
134 | 118, 66, 132, 133 | elrabf 3360 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
135 | 131, 134 | sylibr 224 |
. . . . . . 7
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
136 | 117, 135 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
137 | 136 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
138 | 69, 44 | nfin 3820 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
139 | 138, 71 | nfne 2894 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
140 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
141 | 140 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
142 | 141 | neeq1d 2853 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
143 | 21, 66, 139, 142 | elrabf 3360 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (𝑤 ∈ 𝐴 ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
144 | 143 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
145 | | n0 3931 |
. . . . . . . . . 10
⊢
((⦋𝑤 /
𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
146 | 144, 145 | sylib 208 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
147 | 146 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
148 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
149 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝜑) |
150 | 143 | simplbi 476 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → 𝑤 ∈ 𝐴) |
151 | 150 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝑤 ∈ 𝐴) |
152 | | elinel1 3799 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
153 | 152 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
154 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 ∈ 𝐴) |
155 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴) |
156 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝑉 |
157 | 69, 156 | nfel 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉 |
158 | 155, 157 | nfim 1825 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
159 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
160 | 159 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴))) |
161 | 140 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝐵 ∈ 𝑉 ↔ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)) |
162 | 160, 161 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉))) |
163 | | disjinfi.b |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
164 | 158, 162,
163 | chvar 2262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
165 | 164 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
166 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) |
167 | 166 | elrnmpt1 5374 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝐴 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
168 | 154, 165,
167 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
169 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐵 |
170 | 140 | equcoms 1947 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
171 | 170 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → ⦋𝑤 / 𝑥⦌𝐵 = 𝐵) |
172 | 69, 169, 171 | cbvmpt 4749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
173 | 172 | rneqi 5352 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
174 | 168, 173 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
175 | | elunii 4441 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
176 | 153, 174,
175 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
177 | | elinel2 3800 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐶) |
178 | 177 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐶) |
179 | 176, 178 | elind 3798 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
180 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤 𝑦 ∈ (𝐵 ∩ 𝐶) |
181 | 42, 138 | nfel 2777 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
182 | 141 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
183 | 180, 181,
182 | cbvriota 6621 |
. . . . . . . . . . . . . 14
⊢
(℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
184 | 183 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
185 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
186 | 154, 185 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
187 | | rspe 3003 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
188 | 187 | adantll 750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
189 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝜑) |
190 | | sbequ 2376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
191 | | sbsbc 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
193 | | sbcel2 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶)) |
194 | | csbin 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) |
195 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑧 ∈ V |
196 | | csbconstg 3546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌𝐶 = 𝐶) |
197 | 195, 196 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
⦋𝑧 /
𝑥⦌𝐶 = 𝐶 |
198 | 197 | ineq2i 3811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
199 | 194, 198 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
200 | 199 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
201 | 193, 200 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
202 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
203 | 190, 192,
202 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
204 | 203 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
205 | | equequ2 1953 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑧)) |
206 | 204, 205 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))) |
207 | 206 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
208 | 207 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
209 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) |
210 | 68, 44 | nfin 3820 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
211 | 42, 210 | nfel 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
212 | 181, 211 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
213 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑤 = 𝑧 |
214 | 212, 213 | nfim 1825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
215 | 66, 214 | nfral 2945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
216 | 182 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
217 | | equequ1 1952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑧 ↔ 𝑤 = 𝑧)) |
218 | 216, 217 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
219 | 218 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
220 | 209, 215,
219 | cbvral 3167 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
221 | | biid 251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
222 | | sbsbc 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
223 | | sbcel2 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
224 | | csbin 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) |
225 | | csbco 3543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
226 | | csbconstg 3546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑤⦌𝐶 = 𝐶) |
227 | 195, 226 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌𝐶 = 𝐶 |
228 | 225, 227 | ineq12i 3812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
229 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
230 | 224, 228,
229 | 3eqtri 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
231 | 230 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
232 | 222, 223,
231 | 3bitrri 287 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
233 | 232 | anbi2i 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
234 | 233 | imbi1i 339 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
235 | 234 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑧 ∈
𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
236 | 235 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
237 | 221, 236 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
238 | 208, 220,
237 | 3bitri 286 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
239 | 112, 238 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
240 | 189, 179,
239 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
241 | 188, 240 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
242 | | reu2 3394 |
. . . . . . . . . . . . . . . 16
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
243 | 241, 242 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
244 | | riota1 6629 |
. . . . . . . . . . . . . . 15
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
246 | 186, 245 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤) |
247 | 184, 246 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
248 | 179, 247 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
249 | 248 | ex 450 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
250 | 149, 151,
249 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
251 | 148, 250 | eximd 2085 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
252 | 147, 251 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
253 | | df-rex 2918 |
. . . . . . 7
⊢
(∃𝑦 ∈
(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
254 | 252, 253 | sylibr 224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
255 | 254 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
256 | 137, 255 | jca 554 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
257 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) = (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
258 | 257 | fompt 39379 |
. . . 4
⊢ ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
259 | 256, 258 | sylibr 224 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
260 | | fodomg 9345 |
. . 3
⊢ ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))) |
261 | 11, 259, 260 | sylc 65 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
262 | | domfi 8181 |
. 2
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |
263 | 7, 261, 262 | syl2anc 693 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |