Step | Hyp | Ref
| Expression |
1 | | clcnvlem.ubex |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
2 | | clcnvlem.ssub |
. . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝐴) |
3 | | clcnvlem.clex |
. . . . 5
⊢ (𝜑 → 𝜃) |
4 | 2, 3 | jca 553 |
. . . 4
⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝜃)) |
5 | | clcnvlem.sub3 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) |
6 | 5 | cleq2lem 36933 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) ↔ (𝑋 ⊆ 𝐴 ∧ 𝜃))) |
7 | 1, 4, 6 | elabd 3321 |
. . 3
⊢ (𝜑 → ∃𝑥(𝑋 ⊆ 𝑥 ∧ 𝜓)) |
8 | 7 | cnvintabd 36928 |
. 2
⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑧 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}) |
9 | | df-rab 2905 |
. . . . 5
⊢ {𝑧 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧
∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} |
10 | | exsimpl 1783 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → ∃𝑥 𝑧 = ◡𝑥) |
11 | | relcnv 5422 |
. . . . . . . . . . . . 13
⊢ Rel ◡𝑥 |
12 | | releq 5124 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ◡𝑥 → (Rel 𝑧 ↔ Rel ◡𝑥)) |
13 | 11, 12 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ (𝑧 = ◡𝑥 → Rel 𝑧) |
14 | 13 | exlimiv 1845 |
. . . . . . . . . . 11
⊢
(∃𝑥 𝑧 = ◡𝑥 → Rel 𝑧) |
15 | 10, 14 | syl 17 |
. . . . . . . . . 10
⊢
(∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → Rel 𝑧) |
16 | | df-rel 5045 |
. . . . . . . . . 10
⊢ (Rel
𝑧 ↔ 𝑧 ⊆ (V × V)) |
17 | 15, 16 | sylib 207 |
. . . . . . . . 9
⊢
(∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ⊆ (V × V)) |
18 | | selpw 4115 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝒫 (V × V)
↔ 𝑧 ⊆ (V ×
V)) |
19 | 18 | bicomi 213 |
. . . . . . . . 9
⊢ (𝑧 ⊆ (V × V) ↔
𝑧 ∈ 𝒫 (V
× V)) |
20 | 17, 19 | sylib 207 |
. . . . . . . 8
⊢
(∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → 𝑧 ∈ 𝒫 (V ×
V)) |
21 | 20 | pm4.71ri 663 |
. . . . . . 7
⊢
(∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (𝑧 ∈ 𝒫 (V × V) ∧
∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
22 | 21 | bicomi 213 |
. . . . . 6
⊢ ((𝑧 ∈ 𝒫 (V × V)
∧ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) ↔ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) |
23 | 22 | abbii 2726 |
. . . . 5
⊢ {𝑧 ∣ (𝑧 ∈ 𝒫 (V × V) ∧
∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} |
24 | 9, 23 | eqtri 2632 |
. . . 4
⊢ {𝑧 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} |
25 | 24 | inteqi 4414 |
. . 3
⊢ ∩ {𝑧
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} |
26 | 25 | a1i 11 |
. 2
⊢ (𝜑 → ∩ {𝑧
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}) |
27 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
28 | 27 | cnvex 7006 |
. . . . . 6
⊢ ◡𝑦 ∈ V |
29 | 28 | cnvex 7006 |
. . . . 5
⊢ ◡◡𝑦 ∈ V |
30 | 29 | a1i 11 |
. . . 4
⊢ (𝜑 → ◡◡𝑦 ∈ V) |
31 | 1, 2 | ssexd 4733 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ V) |
32 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ V → (𝑋 ∖ ◡◡𝑋) ∈ V) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∖ ◡◡𝑋) ∈ V) |
34 | | unexg 6857 |
. . . . . . . . . 10
⊢ ((◡𝑦 ∈ V ∧ (𝑋 ∖ ◡◡𝑋) ∈ V) → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V) |
35 | 28, 33, 34 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∈ V) |
36 | | inundif 3998 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 |
37 | | cnvun 5457 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) |
38 | 37 | sseq1i 3592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦) |
39 | 38 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (◡(𝑋 ∩ ◡◡𝑋) ∪ ◡(𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦) |
40 | 39 | unssad 3752 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦) |
41 | | relcnv 5422 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Rel ◡◡𝑋 |
42 | | relin2 5160 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Rel
◡◡𝑋 → Rel (𝑋 ∩ ◡◡𝑋)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Rel
(𝑋 ∩ ◡◡𝑋) |
44 | | dfrel2 5502 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Rel
(𝑋 ∩ ◡◡𝑋) ↔ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋)) |
45 | 43, 44 | mpbi 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ◡◡(𝑋 ∩ ◡◡𝑋) = (𝑋 ∩ ◡◡𝑋) |
46 | | cnvss 5216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → ◡◡(𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦) |
47 | 45, 46 | syl5eqssr 3613 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡(𝑋 ∩ ◡◡𝑋) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦) |
48 | 40, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → (𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦) |
49 | | ssid 3587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋) |
50 | | unss12 3747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∩ ◡◡𝑋) ⊆ ◡𝑦 ∧ (𝑋 ∖ ◡◡𝑋) ⊆ (𝑋 ∖ ◡◡𝑋)) → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
51 | 48, 49, 50 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 → ((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
53 | | cnveq 5218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → ◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = ◡𝑋) |
54 | 53 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ 𝑦 ↔ ◡𝑋 ⊆ 𝑦)) |
55 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
56 | 52, 54, 55 | 3imtr3d 281 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∩ ◡◡𝑋) ∪ (𝑋 ∖ ◡◡𝑋)) = 𝑋 → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
57 | 36, 56 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
58 | | sseq2 3590 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
59 | 57, 58 | syl5ibr 235 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥)) |
60 | 59 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (◡𝑋 ⊆ 𝑦 → 𝑋 ⊆ 𝑥)) |
61 | | clcnvlem.sub1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓)) |
62 | 60, 61 | anim12d 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (𝑋 ⊆ 𝑥 ∧ 𝜓))) |
63 | | cnveq 5218 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡𝑥 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
64 | | cnvun 5457 |
. . . . . . . . . . . . 13
⊢ ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) |
65 | | cnvnonrel 36913 |
. . . . . . . . . . . . . . 15
⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅ |
66 | | 0ss 3924 |
. . . . . . . . . . . . . . 15
⊢ ∅
⊆ ◡◡𝑦 |
67 | 65, 66 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢ ◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 |
68 | | ssequn2 3748 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑋 ∖ ◡◡𝑋) ⊆ ◡◡𝑦 ↔ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦) |
69 | 67, 68 | mpbi 219 |
. . . . . . . . . . . . 13
⊢ (◡◡𝑦 ∪ ◡(𝑋 ∖ ◡◡𝑋)) = ◡◡𝑦 |
70 | 64, 69 | eqtr2i 2633 |
. . . . . . . . . . . 12
⊢ ◡◡𝑦 = ◡(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) |
71 | 63, 70 | syl6reqr 2663 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ◡◡𝑦 = ◡𝑥) |
72 | 71 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ◡◡𝑦 = ◡𝑥) |
73 | 62, 72 | jctild 564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
74 | 35, 73 | spcimedv 3265 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
75 | 74 | imp 444 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) |
76 | 75 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) |
77 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑧 = ◡◡𝑦 → (𝑧 = ◡𝑥 ↔ ◡◡𝑦 = ◡𝑥)) |
78 | 77 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑧 = ◡◡𝑦 → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ (◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
79 | 78 | exbidv 1837 |
. . . . . . 7
⊢ (𝑧 = ◡◡𝑦 → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
80 | 79 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) ↔ ∃𝑥(◡◡𝑦 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
81 | 76, 80 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 = ◡◡𝑦) ∧ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))) |
82 | 81 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = ◡◡𝑦) → ((◡𝑋 ⊆ 𝑦 ∧ 𝜒) → ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)))) |
83 | | cnvcnvss 5507 |
. . . . 5
⊢ ◡◡𝑦 ⊆ 𝑦 |
84 | 83 | a1i 11 |
. . . 4
⊢ (𝜑 → ◡◡𝑦 ⊆ 𝑦) |
85 | 30, 82, 84 | intabssd 36935 |
. . 3
⊢ (𝜑 → ∩ {𝑧
∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} ⊆ ∩
{𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) |
86 | | vex 3176 |
. . . . 5
⊢ 𝑧 ∈ V |
87 | 86 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑧 ∈ V) |
88 | | eqtr 2629 |
. . . . . . . 8
⊢ ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → 𝑦 = ◡𝑥) |
89 | | cnvss 5216 |
. . . . . . . . . . . 12
⊢ (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ ◡𝑥) |
90 | | sseq2 3590 |
. . . . . . . . . . . 12
⊢ (𝑦 = ◡𝑥 → (◡𝑋 ⊆ 𝑦 ↔ ◡𝑋 ⊆ ◡𝑥)) |
91 | 89, 90 | syl5ibr 235 |
. . . . . . . . . . 11
⊢ (𝑦 = ◡𝑥 → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦)) |
92 | 91 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝑋 ⊆ 𝑥 → ◡𝑋 ⊆ 𝑦)) |
93 | | clcnvlem.sub2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒)) |
94 | 92, 93 | anim12d 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))) |
95 | 94 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 = ◡𝑥 → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))) |
96 | 88, 95 | syl5 33 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 = 𝑧 ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒)))) |
97 | 96 | impl 648 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 = 𝑧) ∧ 𝑧 = ◡𝑥) → ((𝑋 ⊆ 𝑥 ∧ 𝜓) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))) |
98 | 97 | expimpd 627 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → ((𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))) |
99 | 98 | exlimdv 1848 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓)) → (◡𝑋 ⊆ 𝑦 ∧ 𝜒))) |
100 | | ssid 3587 |
. . . . 5
⊢ 𝑧 ⊆ 𝑧 |
101 | 100 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑧 ⊆ 𝑧) |
102 | 87, 99, 101 | intabssd 36935 |
. . 3
⊢ (𝜑 → ∩ {𝑦
∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)} ⊆ ∩
{𝑧 ∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))}) |
103 | 85, 102 | eqssd 3585 |
. 2
⊢ (𝜑 → ∩ {𝑧
∣ ∃𝑥(𝑧 = ◡𝑥 ∧ (𝑋 ⊆ 𝑥 ∧ 𝜓))} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) |
104 | 8, 26, 103 | 3eqtrd 2648 |
1
⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) |