Step | Hyp | Ref
| Expression |
1 | | disjinfi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
2 | | inss2 4205 |
. . . 4
⊢ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 |
3 | 2 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Fin → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
4 | | ssfi 8732 |
. . 3
⊢ ((𝐶 ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) → (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
5 | 1, 3, 4 | syl2anc2 587 |
. 2
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
6 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
7 | 6, 1 | jca 514 |
. . . 4
⊢ (𝜑 → ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin)) |
8 | | ssexg 5219 |
. . . 4
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin) → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
10 | | elinel1 4171 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
11 | | eluni2 4835 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
12 | 11 | biimpi 218 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
13 | | vex 3497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
14 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
15 | 14 | elrnmpt 5822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
17 | 16 | biimpi 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
18 | 17 | adantr 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
19 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑤 |
20 | | nfmpt1 5156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
21 | 20 | nfrn 5818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
22 | 19, 21 | nfel 2992 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
23 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑦 ∈ 𝑤 |
24 | 22, 23 | nfan 1896 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) |
25 | | simpl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝑤) |
26 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑤 = 𝐵) |
27 | 25, 26 | eleqtrd 2915 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝐵) |
28 | 27 | ex 415 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝑤 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)) |
29 | 28 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑤 → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
30 | 29 | adantl 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
31 | 24, 30 | reximdai 3311 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
32 | 18, 31 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
33 | 32 | ex 415 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))) |
35 | 34 | rexlimdv 3283 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
36 | 12, 35 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
37 | 10, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
38 | 37 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
39 | | nfv 1911 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜑 |
40 | | nfcv 2977 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑦 |
41 | 21 | nfuni 4838 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
42 | | nfcv 2977 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐶 |
43 | 41, 42 | nfin 4192 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
44 | 40, 43 | nfel 2992 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
45 | 39, 44 | nfan 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
46 | | nfre1 3306 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) |
47 | 2 | sseli 3962 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ 𝐶) |
48 | | simp2 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
49 | | simpr 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
50 | | simpl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐶) |
51 | 49, 50 | elind 4170 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
52 | 51 | 3adant2 1127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
53 | | rspe 3304 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
54 | 48, 52, 53 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
55 | 54 | 3exp 1115 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
56 | 47, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
57 | 56 | adantl 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
58 | 45, 46, 57 | rexlimd 3317 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
59 | 38, 58 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
60 | | disjinfi.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
61 | | disjors 5039 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
62 | 60, 61 | sylib 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
63 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑧∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
64 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥𝐴 |
65 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑧 = 𝑤 |
66 | | nfcsb1v 3906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
67 | 19 | nfcsb1 3905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
68 | 66, 67 | nfin 4192 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) |
69 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥∅ |
70 | 68, 69 | nfeq 2991 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ |
71 | 65, 70 | nfor 1901 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
72 | 64, 71 | nfralw 3225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
73 | | equequ1 2028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
74 | | csbeq1a 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
75 | 74 | ineq1d 4187 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵)) |
76 | 75 | eqeq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
77 | 73, 76 | orbi12d 915 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
78 | 77 | ralbidv 3197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
79 | 63, 72, 78 | cbvralw 3441 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
80 | 62, 79 | sylibr 236 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
81 | | rspa 3206 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
82 | 80, 81 | sylan 582 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
83 | 82 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
84 | | simpr 487 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
85 | | rspa 3206 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
86 | 85 | orcomd 867 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
87 | 83, 84, 86 | syl2anc 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
88 | 87 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
89 | | elinel1 4171 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐵) |
90 | 89 | adantr 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐵) |
91 | | sbsbc 3775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
92 | | sbcel2 4366 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶)) |
93 | | csbin 4390 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋𝑤 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) |
94 | 93 | eleq2i 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
95 | 91, 92, 94 | 3bitri 299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
96 | 95 | biimpi 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
97 | | elinel1 4171 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
99 | 98 | adantl 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
100 | 90, 99 | jca 514 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)) |
101 | | inelcm 4413 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) ≠ ∅) |
102 | 101 | neneqd 3021 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
103 | 100, 102 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
104 | 103 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
105 | | pm2.53 847 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ → 𝑥 = 𝑤)) |
106 | 88, 104, 105 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → 𝑥 = 𝑤) |
107 | 106 | ex 415 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
108 | 107 | ralrimiva 3182 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
109 | 108 | ralrimiva 3182 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
110 | 109 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
111 | 59, 110 | jca 514 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
112 | | reu2 3715 |
. . . . . . . . 9
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
113 | 111, 112 | sylibr 236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
114 | | riotacl2 7124 |
. . . . . . . 8
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
115 | 113, 114 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
116 | | nfriota1 7115 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
117 | 116 | nfcsb1 3905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 |
118 | 117, 42 | nfin 4192 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
119 | 40, 118 | nfel 2992 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑦 ∈
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
120 | | csbeq1a 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝐵 = ⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵) |
121 | 120 | ineq1d 4187 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝐵 ∩ 𝐶) = (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
122 | 121 | eleq2d 2898 |
. . . . . . . . . . . 12
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
123 | 116, 64, 119, 122 | elrabf 3675 |
. . . . . . . . . . 11
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
124 | 123 | biimpi 218 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
125 | 124 | simpld 497 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴) |
126 | 124 | simprd 498 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
127 | 126 | ne0d 4300 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} →
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
128 | 125, 127 | jca 514 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
129 | 118, 69 | nfne 3119 |
. . . . . . . . 9
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
130 | 121 | neeq1d 3075 |
. . . . . . . . 9
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → ((𝐵 ∩ 𝐶) ≠ ∅ ↔
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
131 | 116, 64, 129, 130 | elrabf 3675 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
132 | 128, 131 | sylibr 236 |
. . . . . . 7
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
133 | 115, 132 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
134 | 133 | ralrimiva 3182 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
135 | 67, 42 | nfin 4192 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
136 | 135, 69 | nfne 3119 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
137 | | csbeq1a 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
138 | 137 | ineq1d 4187 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
139 | 138 | neeq1d 3075 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
140 | 19, 64, 136, 139 | elrabf 3675 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (𝑤 ∈ 𝐴 ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
141 | 140 | simprbi 499 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
142 | | n0 4309 |
. . . . . . . . . 10
⊢
((⦋𝑤 /
𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
143 | 141, 142 | sylib 220 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
144 | 143 | adantl 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
145 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
146 | | simpl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝜑) |
147 | 140 | simplbi 500 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → 𝑤 ∈ 𝐴) |
148 | 147 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝑤 ∈ 𝐴) |
149 | | elinel1 4171 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
150 | 149 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
151 | | simplr 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 ∈ 𝐴) |
152 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴) |
153 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝑉 |
154 | 67, 153 | nfel 2992 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉 |
155 | 152, 154 | nfim 1893 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
156 | | eleq1w 2895 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
157 | 156 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴))) |
158 | 137 | eleq1d 2897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝐵 ∈ 𝑉 ↔ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)) |
159 | 157, 158 | imbi12d 347 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉))) |
160 | | disjinfi.b |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
161 | 155, 159,
160 | chvarfv 2238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
162 | 161 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
163 | | eqid 2821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) |
164 | 163 | elrnmpt1 5824 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝐴 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
165 | 151, 162,
164 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
166 | | nfcv 2977 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐵 |
167 | 137 | equcoms 2023 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
168 | 167 | eqcomd 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → ⦋𝑤 / 𝑥⦌𝐵 = 𝐵) |
169 | 67, 166, 168 | cbvmpt 5159 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
170 | 169 | rneqi 5801 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
171 | 165, 170 | eleqtrdi 2923 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
172 | | elunii 4836 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
173 | 150, 171,
172 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
174 | | elinel2 4172 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐶) |
175 | 174 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐶) |
176 | 173, 175 | elind 4170 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
177 | | nfv 1911 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤 𝑦 ∈ (𝐵 ∩ 𝐶) |
178 | 40, 135 | nfel 2992 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
179 | 138 | eleq2d 2898 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
180 | 177, 178,
179 | cbvriotaw 7117 |
. . . . . . . . . . . . . 14
⊢
(℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
181 | 180 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
182 | | simpr 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
183 | 151, 182 | jca 514 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
184 | | rspe 3304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
185 | 184 | adantll 712 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
186 | | simpll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝜑) |
187 | | sbequ 2086 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
188 | | sbsbc 3775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
189 | 188 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
190 | | sbcel2 4366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶)) |
191 | | csbin 4390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) |
192 | | vex 3497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑧 ∈ V |
193 | | csbconstg 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌𝐶 = 𝐶) |
194 | 192, 193 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
⦋𝑧 /
𝑥⦌𝐶 = 𝐶 |
195 | 194 | ineq2i 4185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
196 | 191, 195 | eqtri 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
197 | 196 | eleq2i 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
198 | 190, 197 | bitri 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
200 | 187, 189,
199 | 3bitrd 307 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
201 | 200 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
202 | | equequ2 2029 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑧)) |
203 | 201, 202 | imbi12d 347 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))) |
204 | 203 | cbvralvw 3449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
205 | 204 | ralbii 3165 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
206 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) |
207 | 66, 42 | nfin 4192 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
208 | 40, 207 | nfel 2992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
209 | 178, 208 | nfan 1896 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
210 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑤 = 𝑧 |
211 | 209, 210 | nfim 1893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
212 | 64, 211 | nfralw 3225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
213 | 179 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
214 | | equequ1 2028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑧 ↔ 𝑤 = 𝑧)) |
215 | 213, 214 | imbi12d 347 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
216 | 215 | ralbidv 3197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
217 | 206, 212,
216 | cbvralw 3441 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
218 | | biid 263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
219 | | sbsbc 3775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
220 | | sbcel2 4366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
221 | | csbin 4390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) |
222 | | csbcow 3897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
223 | | csbconstg 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑤⦌𝐶 = 𝐶) |
224 | 192, 223 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌𝐶 = 𝐶 |
225 | 222, 224 | ineq12i 4186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
226 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
227 | 221, 225,
226 | 3eqtri 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
228 | 227 | eleq2i 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
229 | 219, 220,
228 | 3bitrri 300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
230 | 229 | anbi2i 624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
231 | 230 | imbi1i 352 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
232 | 231 | ralbii 3165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑧 ∈
𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
233 | 232 | ralbii 3165 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
234 | 218, 233 | bitri 277 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
235 | 205, 217,
234 | 3bitri 299 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
236 | 110, 235 | sylib 220 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
237 | 186, 176,
236 | syl2anc 586 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
238 | 185, 237 | jca 514 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
239 | | reu2 3715 |
. . . . . . . . . . . . . . . 16
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
240 | 238, 239 | sylibr 236 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
241 | | riota1 7129 |
. . . . . . . . . . . . . . 15
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
243 | 183, 242 | mpbid 234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤) |
244 | 181, 243 | eqtr2d 2857 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
245 | 176, 244 | jca 514 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
246 | 245 | ex 415 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
247 | 146, 148,
246 | syl2anc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
248 | 145, 247 | eximd 2212 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
249 | 144, 248 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
250 | | df-rex 3144 |
. . . . . . 7
⊢
(∃𝑦 ∈
(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
251 | 249, 250 | sylibr 236 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
252 | 251 | ralrimiva 3182 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
253 | 134, 252 | jca 514 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
254 | | eqid 2821 |
. . . . 5
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) = (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
255 | 254 | fompt 41446 |
. . . 4
⊢ ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
256 | 253, 255 | sylibr 236 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
257 | | fodomg 9939 |
. . 3
⊢ ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))) |
258 | 9, 256, 257 | sylc 65 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
259 | | domfi 8733 |
. 2
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |
260 | 5, 258, 259 | syl2anc 586 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |