Step | Hyp | Ref
| Expression |
1 | | disjinfi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
2 | | id 22 |
. . . 4
⊢ (𝐶 ∈ Fin → 𝐶 ∈ Fin) |
3 | | inss2 4057 |
. . . . 5
⊢ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝐶 ∈ Fin → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
5 | | ssfi 8448 |
. . . 4
⊢ ((𝐶 ∈ Fin ∧ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) → (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
6 | 2, 4, 5 | syl2anc 581 |
. . 3
⊢ (𝐶 ∈ Fin → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
7 | 1, 6 | syl 17 |
. 2
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin) |
8 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶) |
9 | 8, 1 | jca 509 |
. . . 4
⊢ (𝜑 → ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin)) |
10 | | ssexg 5028 |
. . . 4
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ⊆ 𝐶 ∧ 𝐶 ∈ Fin) → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V) |
12 | | elinel1 4025 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
13 | | eluni2 4661 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
14 | 13 | biimpi 208 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤) |
15 | | vex 3416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
16 | | eqid 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
17 | 16 | elrnmpt 5604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵)) |
18 | 15, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
19 | 18 | biimpi 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
20 | 19 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑤 = 𝐵) |
21 | | nfcv 2968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑤 |
22 | | nfmpt1 4969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
23 | 22 | nfrn 5600 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
24 | 21, 23 | nfel 2981 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
25 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑦 ∈ 𝑤 |
26 | 24, 25 | nfan 2004 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) |
27 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝑤) |
28 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑤 = 𝐵) |
29 | 27, 28 | eleqtrd 2907 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑤 = 𝐵) → 𝑦 ∈ 𝐵) |
30 | 29 | ex 403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝑤 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵)) |
31 | 30 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑤 → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
32 | 31 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (𝑥 ∈ 𝐴 → (𝑤 = 𝐵 → 𝑦 ∈ 𝐵))) |
33 | 26, 32 | reximdai 3219 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → (∃𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
34 | 20, 33 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑦 ∈ 𝑤) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
35 | 34 | ex 403 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))) |
37 | 36 | rexlimdv 3238 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (∃𝑤 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ∈ 𝑤 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
38 | 14, 37 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
40 | 39 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
41 | | nfv 2015 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜑 |
42 | | nfcv 2968 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑦 |
43 | 23 | nfuni 4663 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
44 | | nfcv 2968 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐶 |
45 | 43, 44 | nfin 4044 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
46 | 42, 45 | nfel 2981 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) |
47 | 41, 46 | nfan 2004 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
48 | | nfre1 3212 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) |
49 | 3 | sseli 3822 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → 𝑦 ∈ 𝐶) |
50 | | simp2 1173 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
51 | | simpr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
52 | | simpl 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐶) |
53 | 51, 52 | elind 4024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
54 | 53 | 3adant2 1167 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ (𝐵 ∩ 𝐶)) |
55 | | rspe 3210 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
56 | 50, 54, 55 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
57 | 56 | 3exp 1154 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
58 | 49, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
59 | 58 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
60 | 47, 48, 59 | rexlimd 3234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
61 | 40, 60 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
62 | | disjinfi.d |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
63 | | disjors 4855 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
64 | 62, 63 | sylib 210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
65 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑧∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
66 | | nfcv 2968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥𝐴 |
67 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑧 = 𝑤 |
68 | | nfcsb1v 3772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
69 | 21 | nfcsb1 3771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
70 | 68, 69 | nfin 4044 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) |
71 | | nfcv 2968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥∅ |
72 | 70, 71 | nfeq 2980 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ |
73 | 67, 72 | nfor 2009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
74 | 66, 73 | nfral 3153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
75 | | equequ1 2131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
76 | | csbeq1a 3765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
77 | 76 | ineq1d 4039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑧 → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵)) |
78 | 77 | eqeq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑧 → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
79 | 75, 78 | orbi12d 949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → ((𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
80 | 79 | ralbidv 3194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅))) |
81 | 65, 74, 80 | cbvral 3378 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 = 𝑤 ∨ (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
82 | 64, 81 | sylibr 226 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
83 | | rspa 3138 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
84 | 82, 83 | sylan 577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
85 | 84 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
86 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
87 | | rspa 3138 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅)) |
88 | 87 | orcomd 904 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑤 ∈
𝐴 (𝑥 = 𝑤 ∨ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
89 | 85, 86, 88 | syl2anc 581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
90 | 89 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤)) |
91 | | elinel1 4025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐵) |
92 | 91 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐵) |
93 | | sbsbc 3665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
94 | | sbcel2 4212 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶)) |
95 | | csbin 4234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋𝑤 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) |
96 | 95 | eleq2i 2897 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ⦋𝑤 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
97 | 93, 94, 96 | 3bitri 289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
98 | 97 | biimpi 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶)) |
99 | | elinel1 4025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
101 | 100 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
102 | 92, 101 | jca 509 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵)) |
103 | | inelcm 4255 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) ≠ ∅) |
104 | 103 | neneqd 3003 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
106 | 105 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → ¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
107 | | pm2.53 884 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ ∨ 𝑥 = 𝑤) → (¬ (𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅ → 𝑥 = 𝑤)) |
108 | 90, 106, 107 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) → 𝑥 = 𝑤) |
109 | 108 | ex 403 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
110 | 109 | ralrimiva 3174 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
111 | 110 | ralrimiva 3174 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
112 | 111 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤)) |
113 | 61, 112 | jca 509 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
114 | | reu2 3618 |
. . . . . . . . 9
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ∧ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤))) |
115 | 113, 114 | sylibr 226 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∃!𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
116 | | riotacl2 6878 |
. . . . . . . 8
⊢
(∃!𝑥 ∈
𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
117 | 115, 116 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)}) |
118 | | nfriota1 6872 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) |
119 | 118 | nfcsb1 3771 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 |
120 | 119, 44 | nfin 4044 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
121 | 42, 120 | nfel 2981 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑦 ∈
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) |
122 | | csbeq1a 3765 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝐵 = ⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵) |
123 | 122 | ineq1d 4039 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝐵 ∩ 𝐶) = (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
124 | 123 | eleq2d 2891 |
. . . . . . . . . . . 12
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
125 | 118, 66, 121, 124 | elrabf 3580 |
. . . . . . . . . . 11
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
126 | 125 | biimpi 208 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶))) |
127 | 126 | simpld 490 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴) |
128 | 126 | simprd 491 |
. . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → 𝑦 ∈ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶)) |
129 | 128 | ne0d 4150 |
. . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} →
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
130 | 127, 129 | jca 509 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
131 | 120, 71 | nfne 3098 |
. . . . . . . . 9
⊢
Ⅎ𝑥(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
132 | 123 | neeq1d 3057 |
. . . . . . . . 9
⊢ (𝑥 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) → ((𝐵 ∩ 𝐶) ≠ ∅ ↔
(⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
133 | 118, 66, 131, 132 | elrabf 3580 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ ((℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ 𝐴 ∧ (⦋(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
134 | 130, 133 | sylibr 226 |
. . . . . . 7
⊢
((℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ 𝑦 ∈ (𝐵 ∩ 𝐶)} → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
135 | 117, 134 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
136 | 135 | ralrimiva 3174 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
137 | 69, 44 | nfin 4044 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
138 | 137, 71 | nfne 3098 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ |
139 | | csbeq1a 3765 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
140 | 139 | ineq1d 4039 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝐶) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
141 | 140 | neeq1d 3057 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ((𝐵 ∩ 𝐶) ≠ ∅ ↔ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
142 | 21, 66, 138, 141 | elrabf 3580 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (𝑤 ∈ 𝐴 ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅)) |
143 | 142 | simprbi 492 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ≠ ∅) |
144 | | n0 4159 |
. . . . . . . . . 10
⊢
((⦋𝑤 /
𝑥⦌𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
145 | 143, 144 | sylib 210 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
146 | 145 | adantl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
147 | | nfv 2015 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
148 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝜑) |
149 | 142 | simplbi 493 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → 𝑤 ∈ 𝐴) |
150 | 149 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → 𝑤 ∈ 𝐴) |
151 | | elinel1 4025 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
152 | 151 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵) |
153 | | simplr 787 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 ∈ 𝐴) |
154 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴) |
155 | | nfcv 2968 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝑉 |
156 | 69, 155 | nfel 2981 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉 |
157 | 154, 156 | nfim 2001 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
158 | | eleq1w 2888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
159 | 158 | anbi2d 624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴))) |
160 | 139 | eleq1d 2890 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝐵 ∈ 𝑉 ↔ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉)) |
161 | 159, 160 | imbi12d 336 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉))) |
162 | | disjinfi.b |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
163 | 157, 161,
162 | chvar 2415 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
164 | 163 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) |
165 | | eqid 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) |
166 | 165 | elrnmpt1 5606 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝐴 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ 𝑉) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
167 | 153, 164,
166 | syl2anc 581 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵)) |
168 | | nfcv 2968 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤𝐵 |
169 | 139 | equcoms 2126 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
170 | 169 | eqcomd 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → ⦋𝑤 / 𝑥⦌𝐵 = 𝐵) |
171 | 69, 168, 170 | cbvmpt 4971 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
172 | 171 | rneqi 5583 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑤 ∈ 𝐴 ↦ ⦋𝑤 / 𝑥⦌𝐵) = ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
173 | 167, 172 | syl6eleq 2915 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
174 | | elunii 4662 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ⦋𝑤 / 𝑥⦌𝐵 ∧ ⦋𝑤 / 𝑥⦌𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
175 | 152, 173,
174 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ ∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)) |
176 | | elinel2 4026 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → 𝑦 ∈ 𝐶) |
177 | 176 | adantl 475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ 𝐶) |
178 | 175, 177 | elind 4024 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
179 | | nfv 2015 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤 𝑦 ∈ (𝐵 ∩ 𝐶) |
180 | 42, 137 | nfel 2981 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) |
181 | 140 | eleq2d 2891 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
182 | 179, 180,
181 | cbvriota 6875 |
. . . . . . . . . . . . . 14
⊢
(℩𝑥
∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) = (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
184 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
185 | 153, 184 | jca 509 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
186 | | rspe 3210 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
187 | 186 | adantll 707 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
188 | | simpll 785 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝜑) |
189 | | sbequ 2506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
190 | | sbsbc 3665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) |
191 | 190 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶))) |
192 | | sbcel2 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶)) |
193 | | csbin 4234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) |
194 | | vex 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑧 ∈ V |
195 | | csbconstg 3769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌𝐶 = 𝐶) |
196 | 194, 195 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
⦋𝑧 /
𝑥⦌𝐶 = 𝐶 |
197 | 196 | ineq2i 4037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
198 | 193, 197 | eqtri 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
199 | 198 | eleq2i 2897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ⦋𝑧 / 𝑥⦌(𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
200 | 192, 199 | bitri 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑧 → ([𝑧 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
202 | 189, 191,
201 | 3bitrd 297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶))) |
203 | 202 | anbi2d 624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
204 | | equequ2 2132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑧)) |
205 | 203, 204 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑧 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧))) |
206 | 205 | cbvralv 3382 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
207 | 206 | ralbii 3188 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧)) |
208 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) |
209 | 68, 44 | nfin 4044 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑥(⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
210 | 42, 209 | nfel 2981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
211 | 180, 210 | nfan 2004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
212 | | nfv 2015 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑤 = 𝑧 |
213 | 211, 212 | nfim 2001 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
214 | 66, 213 | nfral 3153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) |
215 | 181 | anbi1d 625 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)))) |
216 | | equequ1 2131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑧 ↔ 𝑤 = 𝑧)) |
217 | 215, 216 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑤 → (((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
218 | 217 | ralbidv 3194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
219 | 208, 214,
218 | cbvral 3378 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑥 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
220 | | biid 253 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
221 | | sbsbc 3665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
222 | | sbcel2 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
223 | | csbin 4234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) |
224 | | csbco 3766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵 |
225 | | csbconstg 3769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑤⦌𝐶 = 𝐶) |
226 | 194, 225 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
⦋𝑧 /
𝑤⦌𝐶 = 𝐶 |
227 | 224, 226 | ineq12i 4038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑤⦌⦋𝑤 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑤⦌𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
228 | | eqid 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(⦋𝑧 /
𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
229 | 223, 227,
228 | 3eqtri 2852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
⦋𝑧 /
𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) |
230 | 229 | eleq2i 2897 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ⦋𝑧 / 𝑤⦌(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) |
231 | 221, 222,
230 | 3bitrri 290 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶) ↔ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
232 | 231 | anbi2i 618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶))) |
233 | 232 | imbi1i 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
234 | 233 | ralbii 3188 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑧 ∈
𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
235 | 234 | ralbii 3188 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
236 | 220, 235 | bitri 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ 𝑦 ∈ (⦋𝑧 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
237 | 207, 219,
236 | 3bitri 289 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 ((𝑦 ∈ (𝐵 ∩ 𝐶) ∧ [𝑤 / 𝑥]𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑥 = 𝑤) ↔ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
238 | 112, 237 | sylib 210 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
239 | 188, 178,
238 | syl2anc 581 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧)) |
240 | 187, 239 | jca 509 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
241 | | reu2 3618 |
. . . . . . . . . . . . . . . 16
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ↔ (∃𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ ∀𝑤 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) ∧ [𝑧 / 𝑤]𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = 𝑧))) |
242 | 240, 241 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ∃!𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) |
243 | | riota1 6883 |
. . . . . . . . . . . . . . 15
⊢
(∃!𝑤 ∈
𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → ((𝑤 ∈ 𝐴 ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) ↔ (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤)) |
245 | 185, 244 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (℩𝑤 ∈ 𝐴 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) = 𝑤) |
246 | 183, 245 | eqtr2d 2861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
247 | 178, 246 | jca 509 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶)) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
248 | 247 | ex 403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
249 | 148, 150,
248 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
250 | 147, 249 | eximd 2261 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → (∃𝑦 𝑦 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝐶) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))))) |
251 | 146, 250 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
252 | | df-rex 3122 |
. . . . . . 7
⊢
(∃𝑦 ∈
(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ↔ ∃𝑦(𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∧ 𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
253 | 251, 252 | sylibr 226 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) → ∃𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
254 | 253 | ralrimiva 3174 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
255 | 136, 254 | jca 509 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
256 | | eqid 2824 |
. . . . 5
⊢ (𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) = (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))) |
257 | 256 | fompt 40186 |
. . . 4
⊢ ((𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ↔ (∀𝑦 ∈ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)(℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∧ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}∃𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)𝑤 = (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
258 | 255, 257 | sylibr 226 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅}) |
259 | | fodomg 9659 |
. . 3
⊢ ((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ V → ((𝑦 ∈ (∪ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ↦ (℩𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))):(∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)–onto→{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶))) |
260 | 11, 258, 259 | sylc 65 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) |
261 | | domfi 8449 |
. 2
⊢ (((∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶) ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ≼ (∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∩ 𝐶)) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |
262 | 7, 260, 261 | syl2anc 581 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) |