Step | Hyp | Ref
| Expression |
1 | | fin1aufil.1 |
. . . . . . 7
⊢ 𝐹 = (𝒫 𝑋 ∖ Fin) |
2 | 1 | eleq2i 2680 |
. . . . . 6
⊢ (𝑥 ∈ 𝐹 ↔ 𝑥 ∈ (𝒫 𝑋 ∖ Fin)) |
3 | | eldif 3550 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑥 ∈ 𝒫 𝑋 ∧ ¬ 𝑥 ∈ Fin)) |
4 | | selpw 4115 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
5 | 4 | anbi1i 727 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 𝑋 ∧ ¬ 𝑥 ∈ Fin) ↔ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin)) |
6 | 2, 3, 5 | 3bitri 285 |
. . . . 5
⊢ (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin)) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ (FinIa
∖ Fin) → (𝑥
∈ 𝐹 ↔ (𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin))) |
8 | | elex 3185 |
. . . 4
⊢ (𝑋 ∈ (FinIa
∖ Fin) → 𝑋
∈ V) |
9 | | eldifn 3695 |
. . . . 5
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ¬ 𝑋
∈ Fin) |
10 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ∈ Fin ↔ 𝑋 ∈ Fin)) |
11 | 10 | notbid 307 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin)) |
12 | 11 | sbcieg 3435 |
. . . . 5
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ([𝑋 / 𝑥] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin)) |
13 | 9, 12 | mpbird 246 |
. . . 4
⊢ (𝑋 ∈ (FinIa
∖ Fin) → [𝑋 / 𝑥] ¬ 𝑥 ∈ Fin) |
14 | | 0fin 8073 |
. . . . . 6
⊢ ∅
∈ Fin |
15 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
16 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑥 ∈ Fin ↔ ∅
∈ Fin)) |
17 | 16 | notbid 307 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (¬ 𝑥 ∈ Fin ↔ ¬ ∅
∈ Fin)) |
18 | 15, 17 | sbcie 3437 |
. . . . . . 7
⊢
([∅ / 𝑥] ¬ 𝑥 ∈ Fin ↔ ¬ ∅ ∈
Fin) |
19 | 18 | con2bii 346 |
. . . . . 6
⊢ (∅
∈ Fin ↔ ¬ [∅ / 𝑥] ¬ 𝑥 ∈ Fin) |
20 | 14, 19 | mpbi 219 |
. . . . 5
⊢ ¬
[∅ / 𝑥]
¬ 𝑥 ∈
Fin |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ¬ [∅ / 𝑥] ¬ 𝑥 ∈ Fin) |
22 | | ssfi 8065 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ 𝑧 ⊆ 𝑦) → 𝑧 ∈ Fin) |
23 | 22 | expcom 450 |
. . . . . . 7
⊢ (𝑧 ⊆ 𝑦 → (𝑦 ∈ Fin → 𝑧 ∈ Fin)) |
24 | 23 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∈ Fin → 𝑧 ∈ Fin)) |
25 | 24 | con3d 147 |
. . . . 5
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦) → (¬ 𝑧 ∈ Fin → ¬ 𝑦 ∈ Fin)) |
26 | | vex 3176 |
. . . . . 6
⊢ 𝑧 ∈ V |
27 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ Fin ↔ 𝑧 ∈ Fin)) |
28 | 27 | notbid 307 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (¬ 𝑥 ∈ Fin ↔ ¬ 𝑧 ∈ Fin)) |
29 | 26, 28 | sbcie 3437 |
. . . . 5
⊢
([𝑧 / 𝑥] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑧 ∈ Fin) |
30 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
31 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ Fin ↔ 𝑦 ∈ Fin)) |
32 | 31 | notbid 307 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ Fin ↔ ¬ 𝑦 ∈ Fin)) |
33 | 30, 32 | sbcie 3437 |
. . . . 5
⊢
([𝑦 / 𝑥] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑦 ∈ Fin) |
34 | 25, 29, 33 | 3imtr4g 284 |
. . . 4
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦) → ([𝑧 / 𝑥] ¬ 𝑥 ∈ Fin → [𝑦 / 𝑥] ¬ 𝑥 ∈ Fin)) |
35 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑋 ∈ (FinIa
∖ Fin) → 𝑋
∈ FinIa) |
36 | | fin1ai 8998 |
. . . . . . . . 9
⊢ ((𝑋 ∈ FinIa ∧
𝑦 ⊆ 𝑋) → (𝑦 ∈ Fin ∨ (𝑋 ∖ 𝑦) ∈ Fin)) |
37 | 35, 36 | sylan 487 |
. . . . . . . 8
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋) → (𝑦 ∈ Fin ∨ (𝑋 ∖ 𝑦) ∈ Fin)) |
38 | 37 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) → (𝑦 ∈ Fin ∨ (𝑋 ∖ 𝑦) ∈ Fin)) |
39 | | inundif 3998 |
. . . . . . . . . . 11
⊢ ((𝑧 ∩ 𝑦) ∪ (𝑧 ∖ 𝑦)) = 𝑧 |
40 | | incom 3767 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∩ 𝑦) = (𝑦 ∩ 𝑧) |
41 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → (𝑦 ∩ 𝑧) ∈ Fin) |
42 | 40, 41 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → (𝑧 ∩ 𝑦) ∈ Fin) |
43 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → (𝑋 ∖ 𝑦) ∈ Fin) |
44 | | simpl3 1059 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → 𝑧 ⊆ 𝑋) |
45 | 44 | ssdifd 3708 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → (𝑧 ∖ 𝑦) ⊆ (𝑋 ∖ 𝑦)) |
46 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∖ 𝑦) ∈ Fin ∧ (𝑧 ∖ 𝑦) ⊆ (𝑋 ∖ 𝑦)) → (𝑧 ∖ 𝑦) ∈ Fin) |
47 | 43, 45, 46 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → (𝑧 ∖ 𝑦) ∈ Fin) |
48 | | unfi 8112 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∩ 𝑦) ∈ Fin ∧ (𝑧 ∖ 𝑦) ∈ Fin) → ((𝑧 ∩ 𝑦) ∪ (𝑧 ∖ 𝑦)) ∈ Fin) |
49 | 42, 47, 48 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → ((𝑧 ∩ 𝑦) ∪ (𝑧 ∖ 𝑦)) ∈ Fin) |
50 | 39, 49 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ ((𝑦 ∩ 𝑧) ∈ Fin ∧ (𝑋 ∖ 𝑦) ∈ Fin)) → 𝑧 ∈ Fin) |
51 | 50 | expr 641 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ (𝑦 ∩ 𝑧) ∈ Fin) → ((𝑋 ∖ 𝑦) ∈ Fin → 𝑧 ∈ Fin)) |
52 | 51 | orim2d 881 |
. . . . . . . 8
⊢ (((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) ∧ (𝑦 ∩ 𝑧) ∈ Fin) → ((𝑦 ∈ Fin ∨ (𝑋 ∖ 𝑦) ∈ Fin) → (𝑦 ∈ Fin ∨ 𝑧 ∈ Fin))) |
53 | 52 | ex 449 |
. . . . . . 7
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) → ((𝑦 ∩ 𝑧) ∈ Fin → ((𝑦 ∈ Fin ∨ (𝑋 ∖ 𝑦) ∈ Fin) → (𝑦 ∈ Fin ∨ 𝑧 ∈ Fin)))) |
54 | 38, 53 | mpid 43 |
. . . . . 6
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) → ((𝑦 ∩ 𝑧) ∈ Fin → (𝑦 ∈ Fin ∨ 𝑧 ∈ Fin))) |
55 | 54 | con3d 147 |
. . . . 5
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) → (¬ (𝑦 ∈ Fin ∨ 𝑧 ∈ Fin) → ¬ (𝑦 ∩ 𝑧) ∈ Fin)) |
56 | 33, 29 | anbi12i 729 |
. . . . . 6
⊢
(([𝑦 / 𝑥] ¬ 𝑥 ∈ Fin ∧ [𝑧 / 𝑥] ¬ 𝑥 ∈ Fin) ↔ (¬ 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ Fin)) |
57 | | ioran 510 |
. . . . . 6
⊢ (¬
(𝑦 ∈ Fin ∨ 𝑧 ∈ Fin) ↔ (¬ 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ Fin)) |
58 | 56, 57 | bitr4i 266 |
. . . . 5
⊢
(([𝑦 / 𝑥] ¬ 𝑥 ∈ Fin ∧ [𝑧 / 𝑥] ¬ 𝑥 ∈ Fin) ↔ ¬ (𝑦 ∈ Fin ∨ 𝑧 ∈ Fin)) |
59 | 30 | inex1 4727 |
. . . . . 6
⊢ (𝑦 ∩ 𝑧) ∈ V |
60 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝑥 ∈ Fin ↔ (𝑦 ∩ 𝑧) ∈ Fin)) |
61 | 60 | notbid 307 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (¬ 𝑥 ∈ Fin ↔ ¬ (𝑦 ∩ 𝑧) ∈ Fin)) |
62 | 59, 61 | sbcie 3437 |
. . . . 5
⊢
([(𝑦 ∩
𝑧) / 𝑥] ¬ 𝑥 ∈ Fin ↔ ¬ (𝑦 ∩ 𝑧) ∈ Fin) |
63 | 55, 58, 62 | 3imtr4g 284 |
. . . 4
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑦
⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋) → (([𝑦 / 𝑥] ¬ 𝑥 ∈ Fin ∧ [𝑧 / 𝑥] ¬ 𝑥 ∈ Fin) → [(𝑦 ∩ 𝑧) / 𝑥] ¬ 𝑥 ∈ Fin)) |
64 | 7, 8, 13, 21, 34, 63 | isfild 21472 |
. . 3
⊢ (𝑋 ∈ (FinIa
∖ Fin) → 𝐹
∈ (Fil‘𝑋)) |
65 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ¬
𝑋 ∈
Fin) |
66 | | unfi 8112 |
. . . . . . . 8
⊢ ((𝑥 ∈ Fin ∧ (𝑋 ∖ 𝑥) ∈ Fin) → (𝑥 ∪ (𝑋 ∖ 𝑥)) ∈ Fin) |
67 | | ssun2 3739 |
. . . . . . . . 9
⊢ 𝑋 ⊆ (𝑥 ∪ 𝑋) |
68 | | undif2 3996 |
. . . . . . . . 9
⊢ (𝑥 ∪ (𝑋 ∖ 𝑥)) = (𝑥 ∪ 𝑋) |
69 | 67, 68 | sseqtr4i 3601 |
. . . . . . . 8
⊢ 𝑋 ⊆ (𝑥 ∪ (𝑋 ∖ 𝑥)) |
70 | | ssfi 8065 |
. . . . . . . 8
⊢ (((𝑥 ∪ (𝑋 ∖ 𝑥)) ∈ Fin ∧ 𝑋 ⊆ (𝑥 ∪ (𝑋 ∖ 𝑥))) → 𝑋 ∈ Fin) |
71 | 66, 69, 70 | sylancl 693 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ (𝑋 ∖ 𝑥) ∈ Fin) → 𝑋 ∈ Fin) |
72 | 65, 71 | nsyl 134 |
. . . . . 6
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ¬
(𝑥 ∈ Fin ∧ (𝑋 ∖ 𝑥) ∈ Fin)) |
73 | | ianor 508 |
. . . . . 6
⊢ (¬
(𝑥 ∈ Fin ∧ (𝑋 ∖ 𝑥) ∈ Fin) ↔ (¬ 𝑥 ∈ Fin ∨ ¬ (𝑋 ∖ 𝑥) ∈ Fin)) |
74 | 72, 73 | sylib 207 |
. . . . 5
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → (¬
𝑥 ∈ Fin ∨ ¬
(𝑋 ∖ 𝑥) ∈ Fin)) |
75 | | elpwi 4117 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
76 | 75 | adantl 481 |
. . . . . . 7
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → 𝑥 ⊆ 𝑋) |
77 | 6 | baib 942 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin)) |
78 | 76, 77 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → (𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin)) |
79 | 1 | eleq2i 2680 |
. . . . . . 7
⊢ ((𝑋 ∖ 𝑥) ∈ 𝐹 ↔ (𝑋 ∖ 𝑥) ∈ (𝒫 𝑋 ∖ Fin)) |
80 | | difss 3699 |
. . . . . . . . 9
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 |
81 | | elpw2g 4754 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ((𝑋
∖ 𝑥) ∈ 𝒫
𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
82 | 81 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
83 | 80, 82 | mpbiri 247 |
. . . . . . . 8
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
84 | | eldif 3550 |
. . . . . . . . 9
⊢ ((𝑋 ∖ 𝑥) ∈ (𝒫 𝑋 ∖ Fin) ↔ ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ∧ ¬ (𝑋 ∖ 𝑥) ∈ Fin)) |
85 | 84 | baib 942 |
. . . . . . . 8
⊢ ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 → ((𝑋 ∖ 𝑥) ∈ (𝒫 𝑋 ∖ Fin) ↔ ¬ (𝑋 ∖ 𝑥) ∈ Fin)) |
86 | 83, 85 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ((𝑋 ∖ 𝑥) ∈ (𝒫 𝑋 ∖ Fin) ↔ ¬ (𝑋 ∖ 𝑥) ∈ Fin)) |
87 | 79, 86 | syl5bb 271 |
. . . . . 6
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 ↔ ¬ (𝑋 ∖ 𝑥) ∈ Fin)) |
88 | 78, 87 | orbi12d 742 |
. . . . 5
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) ↔ (¬ 𝑥 ∈ Fin ∨ ¬ (𝑋 ∖ 𝑥) ∈ Fin))) |
89 | 74, 88 | mpbird 246 |
. . . 4
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
𝒫 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
90 | 89 | ralrimiva 2949 |
. . 3
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
91 | | isufil 21517 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹))) |
92 | 64, 90, 91 | sylanbrc 695 |
. 2
⊢ (𝑋 ∈ (FinIa
∖ Fin) → 𝐹
∈ (UFil‘𝑋)) |
93 | | snfi 7923 |
. . . . 5
⊢ {𝑥} ∈ Fin |
94 | | eldifn 3695 |
. . . . . 6
⊢ ({𝑥} ∈ (𝒫 𝑋 ∖ Fin) → ¬
{𝑥} ∈
Fin) |
95 | 94, 1 | eleq2s 2706 |
. . . . 5
⊢ ({𝑥} ∈ 𝐹 → ¬ {𝑥} ∈ Fin) |
96 | 93, 95 | mt2 190 |
. . . 4
⊢ ¬
{𝑥} ∈ 𝐹 |
97 | | uffixsn 21539 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ∈ ∩ 𝐹) → {𝑥} ∈ 𝐹) |
98 | 92, 97 | sylan 487 |
. . . . 5
⊢ ((𝑋 ∈ (FinIa
∖ Fin) ∧ 𝑥 ∈
∩ 𝐹) → {𝑥} ∈ 𝐹) |
99 | 98 | ex 449 |
. . . 4
⊢ (𝑋 ∈ (FinIa
∖ Fin) → (𝑥
∈ ∩ 𝐹 → {𝑥} ∈ 𝐹)) |
100 | 96, 99 | mtoi 189 |
. . 3
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ¬ 𝑥
∈ ∩ 𝐹) |
101 | 100 | eq0rdv 3931 |
. 2
⊢ (𝑋 ∈ (FinIa
∖ Fin) → ∩ 𝐹 = ∅) |
102 | 92, 101 | jca 553 |
1
⊢ (𝑋 ∈ (FinIa
∖ Fin) → (𝐹
∈ (UFil‘𝑋) ∧
∩ 𝐹 = ∅)) |