Step | Hyp | Ref
| Expression |
1 | | difeq2 3684 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
2 | 1 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ 𝑦) ∈ Fin)) |
3 | 2 | elrab 3331 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ↔ (𝑦 ∈ 𝒫 𝑋 ∧ (𝐴 ∖ 𝑦) ∈ Fin)) |
4 | | selpw 4115 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋) |
5 | 4 | anbi1i 727 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 𝑋 ∧ (𝐴 ∖ 𝑦) ∈ Fin) ↔ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∖ 𝑦) ∈ Fin)) |
6 | 3, 5 | bitri 263 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ↔ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∖ 𝑦) ∈ Fin)) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ↔ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∖ 𝑦) ∈ Fin))) |
8 | | elex 3185 |
. . 3
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V) |
9 | 8 | 3ad2ant1 1075 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → 𝑋 ∈ V) |
10 | | ssdif0 3896 |
. . . . 5
⊢ (𝐴 ⊆ 𝑋 ↔ (𝐴 ∖ 𝑋) = ∅) |
11 | | 0fin 8073 |
. . . . . 6
⊢ ∅
∈ Fin |
12 | | eleq1 2676 |
. . . . . 6
⊢ ((𝐴 ∖ 𝑋) = ∅ → ((𝐴 ∖ 𝑋) ∈ Fin ↔ ∅ ∈
Fin)) |
13 | 11, 12 | mpbiri 247 |
. . . . 5
⊢ ((𝐴 ∖ 𝑋) = ∅ → (𝐴 ∖ 𝑋) ∈ Fin) |
14 | 10, 13 | sylbi 206 |
. . . 4
⊢ (𝐴 ⊆ 𝑋 → (𝐴 ∖ 𝑋) ∈ Fin) |
15 | | difeq2 3684 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (𝐴 ∖ 𝑦) = (𝐴 ∖ 𝑋)) |
16 | 15 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = 𝑋 → ((𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑋) ∈ Fin)) |
17 | 16 | sbcieg 3435 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑋) ∈ Fin)) |
18 | 17 | biimpar 501 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ (𝐴 ∖ 𝑋) ∈ Fin) → [𝑋 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) |
19 | 14, 18 | sylan2 490 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋) → [𝑋 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) |
20 | 19 | 3adant3 1074 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → [𝑋 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) |
21 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
22 | | difeq2 3684 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝐴 ∖ 𝑦) = (𝐴 ∖ ∅)) |
23 | 22 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = ∅ → ((𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ ∅) ∈
Fin)) |
24 | 21, 23 | sbcie 3437 |
. . . . 5
⊢
([∅ / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ ∅) ∈
Fin) |
25 | | dif0 3904 |
. . . . . 6
⊢ (𝐴 ∖ ∅) = 𝐴 |
26 | 25 | eleq1i 2679 |
. . . . 5
⊢ ((𝐴 ∖ ∅) ∈ Fin
↔ 𝐴 ∈
Fin) |
27 | 24, 26 | sylbb 208 |
. . . 4
⊢
([∅ / 𝑦](𝐴 ∖ 𝑦) ∈ Fin → 𝐴 ∈ Fin) |
28 | 27 | con3i 149 |
. . 3
⊢ (¬
𝐴 ∈ Fin → ¬
[∅ / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) |
29 | 28 | 3ad2ant3 1077 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ¬ [∅ /
𝑦](𝐴 ∖ 𝑦) ∈ Fin) |
30 | | sscon 3706 |
. . . . 5
⊢ (𝑤 ⊆ 𝑧 → (𝐴 ∖ 𝑧) ⊆ (𝐴 ∖ 𝑤)) |
31 | | ssfi 8065 |
. . . . . 6
⊢ (((𝐴 ∖ 𝑤) ∈ Fin ∧ (𝐴 ∖ 𝑧) ⊆ (𝐴 ∖ 𝑤)) → (𝐴 ∖ 𝑧) ∈ Fin) |
32 | 31 | expcom 450 |
. . . . 5
⊢ ((𝐴 ∖ 𝑧) ⊆ (𝐴 ∖ 𝑤) → ((𝐴 ∖ 𝑤) ∈ Fin → (𝐴 ∖ 𝑧) ∈ Fin)) |
33 | 30, 32 | syl 17 |
. . . 4
⊢ (𝑤 ⊆ 𝑧 → ((𝐴 ∖ 𝑤) ∈ Fin → (𝐴 ∖ 𝑧) ∈ Fin)) |
34 | | vex 3176 |
. . . . 5
⊢ 𝑤 ∈ V |
35 | | difeq2 3684 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝐴 ∖ 𝑦) = (𝐴 ∖ 𝑤)) |
36 | 35 | eleq1d 2672 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑤) ∈ Fin)) |
37 | 34, 36 | sbcie 3437 |
. . . 4
⊢
([𝑤 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑤) ∈ Fin) |
38 | | vex 3176 |
. . . . 5
⊢ 𝑧 ∈ V |
39 | | difeq2 3684 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝐴 ∖ 𝑦) = (𝐴 ∖ 𝑧)) |
40 | 39 | eleq1d 2672 |
. . . . 5
⊢ (𝑦 = 𝑧 → ((𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑧) ∈ Fin)) |
41 | 38, 40 | sbcie 3437 |
. . . 4
⊢
([𝑧 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ 𝑧) ∈ Fin) |
42 | 33, 37, 41 | 3imtr4g 284 |
. . 3
⊢ (𝑤 ⊆ 𝑧 → ([𝑤 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin → [𝑧 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin)) |
43 | 42 | 3ad2ant3 1077 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin → [𝑧 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin)) |
44 | | difindi 3840 |
. . . . 5
⊢ (𝐴 ∖ (𝑧 ∩ 𝑤)) = ((𝐴 ∖ 𝑧) ∪ (𝐴 ∖ 𝑤)) |
45 | | unfi 8112 |
. . . . 5
⊢ (((𝐴 ∖ 𝑧) ∈ Fin ∧ (𝐴 ∖ 𝑤) ∈ Fin) → ((𝐴 ∖ 𝑧) ∪ (𝐴 ∖ 𝑤)) ∈ Fin) |
46 | 44, 45 | syl5eqel 2692 |
. . . 4
⊢ (((𝐴 ∖ 𝑧) ∈ Fin ∧ (𝐴 ∖ 𝑤) ∈ Fin) → (𝐴 ∖ (𝑧 ∩ 𝑤)) ∈ Fin) |
47 | 46 | a1i 11 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (((𝐴 ∖ 𝑧) ∈ Fin ∧ (𝐴 ∖ 𝑤) ∈ Fin) → (𝐴 ∖ (𝑧 ∩ 𝑤)) ∈ Fin)) |
48 | 41, 37 | anbi12i 729 |
. . 3
⊢
(([𝑧 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ∧ [𝑤 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) ↔ ((𝐴 ∖ 𝑧) ∈ Fin ∧ (𝐴 ∖ 𝑤) ∈ Fin)) |
49 | 38 | inex1 4727 |
. . . 4
⊢ (𝑧 ∩ 𝑤) ∈ V |
50 | | difeq2 3684 |
. . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (𝑧 ∩ 𝑤))) |
51 | 50 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = (𝑧 ∩ 𝑤) → ((𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ (𝑧 ∩ 𝑤)) ∈ Fin)) |
52 | 49, 51 | sbcie 3437 |
. . 3
⊢
([(𝑧 ∩
𝑤) / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ↔ (𝐴 ∖ (𝑧 ∩ 𝑤)) ∈ Fin) |
53 | 47, 48, 52 | 3imtr4g 284 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋) → (([𝑧 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin ∧ [𝑤 / 𝑦](𝐴 ∖ 𝑦) ∈ Fin) → [(𝑧 ∩ 𝑤) / 𝑦](𝐴 ∖ 𝑦) ∈ Fin)) |
54 | 7, 9, 20, 29, 43, 53 | isfild 21472 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋)) |