MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  filuni Structured version   Visualization version   GIF version

Theorem filuni 23880
Description: The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
filuni ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Distinct variable groups:   𝑓,𝑔,𝐹   𝑓,𝑋,𝑔

Proof of Theorem filuni
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni2 4917 . . . 4 (𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
2 ssel2 3974 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓 ∈ (Fil‘𝑋))
3 filelss 23847 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
43ex 411 . . . . . . 7 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
52, 4syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (𝑥𝑓𝑥𝑋))
65rexlimdva 3145 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
763ad2ant1 1130 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
81, 7biimtrid 241 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹𝑥𝑋))
98pm4.71rd 561 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹 ↔ (𝑥𝑋𝑥 𝐹)))
10 ssn0 4405 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (Fil‘𝑋) ≠ ∅)
11 fvprc 6893 . . . . 5 𝑋 ∈ V → (Fil‘𝑋) = ∅)
1211necon1ai 2958 . . . 4 ((Fil‘𝑋) ≠ ∅ → 𝑋 ∈ V)
1310, 12syl 17 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → 𝑋 ∈ V)
14133adant3 1129 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 ∈ V)
15 filtop 23850 . . . . . . . . 9 (𝑓 ∈ (Fil‘𝑋) → 𝑋𝑓)
162, 15syl 17 . . . . . . . 8 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑋𝑓)
1716a1d 25 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑋𝑓))
1817ralimdva 3157 . . . . . 6 (𝐹 ⊆ (Fil‘𝑋) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∀𝑓𝐹 𝑋𝑓))
19 r19.2z 4499 . . . . . . 7 ((𝐹 ≠ ∅ ∧ ∀𝑓𝐹 𝑋𝑓) → ∃𝑓𝐹 𝑋𝑓)
2019ex 411 . . . . . 6 (𝐹 ≠ ∅ → (∀𝑓𝐹 𝑋𝑓 → ∃𝑓𝐹 𝑋𝑓))
2118, 20sylan9 506 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∃𝑓𝐹 𝑋𝑓))
22213impia 1114 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∃𝑓𝐹 𝑋𝑓)
23 eluni2 4917 . . . 4 (𝑋 𝐹 ↔ ∃𝑓𝐹 𝑋𝑓)
2422, 23sylibr 233 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 𝐹)
25 sbcel1v 3847 . . 3 ([𝑋 / 𝑥]𝑥 𝐹𝑋 𝐹)
2624, 25sylibr 233 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → [𝑋 / 𝑥]𝑥 𝐹)
27 0nelfil 23844 . . . . . 6 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
282, 27syl 17 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → ¬ ∅ ∈ 𝑓)
2928ralrimiva 3136 . . . 4 (𝐹 ⊆ (Fil‘𝑋) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
30293ad2ant1 1130 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
31 sbcel1v 3847 . . . . . 6 ([∅ / 𝑥]𝑥 𝐹 ↔ ∅ ∈ 𝐹)
32 eluni2 4917 . . . . . 6 (∅ ∈ 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3331, 32bitri 274 . . . . 5 ([∅ / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3433notbii 319 . . . 4 [∅ / 𝑥]𝑥 𝐹 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
35 ralnex 3062 . . . 4 (∀𝑓𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
3634, 35bitr4i 277 . . 3 [∅ / 𝑥]𝑥 𝐹 ↔ ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
3730, 36sylibr 233 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ¬ [∅ / 𝑥]𝑥 𝐹)
38 simp13 1202 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
39 r19.29 3104 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑥𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))
4039ex 411 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
4138, 40syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
42 simp1 1133 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ⊆ (Fil‘𝑋))
43 simp1 1133 . . . . . . . . 9 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → 𝐹 ⊆ (Fil‘𝑋))
44 simpl 481 . . . . . . . . 9 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)) → 𝑓𝐹)
4543, 44, 2syl2an 594 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑓 ∈ (Fil‘𝑋))
46 simprrr 780 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑓)
47 simpl2 1189 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑋)
48 simpl3 1190 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑦)
49 filss 23848 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ (𝑥𝑓𝑦𝑋𝑥𝑦)) → 𝑦𝑓)
5045, 46, 47, 48, 49syl13anc 1369 . . . . . . 7 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑓)
5150expr 455 . . . . . 6 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ 𝑓𝐹) → ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → 𝑦𝑓))
5251reximdva 3158 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5342, 52syl3an1 1160 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5441, 53syld 47 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 𝑦𝑓))
55 sbcel1v 3847 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹𝑥 𝐹)
5655, 1bitri 274 . . 3 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
57 sbcel1v 3847 . . . 4 ([𝑦 / 𝑥]𝑥 𝐹𝑦 𝐹)
58 eluni2 4917 . . . 4 (𝑦 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
5957, 58bitri 274 . . 3 ([𝑦 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
6054, 56, 593imtr4g 295 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ([𝑥 / 𝑥]𝑥 𝐹[𝑦 / 𝑥]𝑥 𝐹))
61 simp13 1202 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
62 r19.29 3104 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑦𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓))
6362ex 411 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
6461, 63syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
65 simp11 1200 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → 𝐹 ⊆ (Fil‘𝑋))
66 r19.29 3104 . . . . . . . . . . 11 ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔))
6766ex 411 . . . . . . . . . 10 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔)))
68 elun1 4177 . . . . . . . . . . . . . . . 16 (𝑦𝑓𝑦 ∈ (𝑓𝑔))
69 elun2 4178 . . . . . . . . . . . . . . . 16 (𝑥𝑔𝑥 ∈ (𝑓𝑔))
7068, 69anim12i 611 . . . . . . . . . . . . . . 15 ((𝑦𝑓𝑥𝑔) → (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔)))
71 eleq2 2815 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑦𝑦 ∈ (𝑓𝑔)))
72 eleq2 2815 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑥𝑥 ∈ (𝑓𝑔)))
7371, 72anbi12d 630 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑔) → ((𝑦𝑥) ↔ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))))
7473rspcev 3608 . . . . . . . . . . . . . . 15 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))) → ∃𝐹 (𝑦𝑥))
7570, 74sylan2 591 . . . . . . . . . . . . . 14 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦𝑓𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7675an12s 647 . . . . . . . . . . . . 13 ((𝑦𝑓 ∧ ((𝑓𝑔) ∈ 𝐹𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7776ex 411 . . . . . . . . . . . 12 (𝑦𝑓 → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7877ad2antlr 725 . . . . . . . . . . 11 (((𝑓𝐹𝑦𝑓) ∧ 𝑔𝐹) → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7978rexlimdva 3145 . . . . . . . . . 10 ((𝑓𝐹𝑦𝑓) → (∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
8067, 79syl9r 78 . . . . . . . . 9 ((𝑓𝐹𝑦𝑓) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥))))
8180impr 453 . . . . . . . 8 ((𝑓𝐹 ∧ (𝑦𝑓 ∧ ∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8281ancom2s 648 . . . . . . 7 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8382rexlimiva 3137 . . . . . 6 (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8483imp 405 . . . . 5 ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥))
85 ssel2 3974 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ∈ (Fil‘𝑋))
86 filin 23849 . . . . . . . 8 (( ∈ (Fil‘𝑋) ∧ 𝑦𝑥) → (𝑦𝑥) ∈ )
87863expib 1119 . . . . . . 7 ( ∈ (Fil‘𝑋) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8885, 87syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8988reximdva 3158 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝐹 (𝑦𝑥) → ∃𝐹 (𝑦𝑥) ∈ ))
9065, 84, 89syl2im 40 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
9164, 90syland 601 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
92 eluni2 4917 . . . . 5 (𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9355, 92bitri 274 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9459, 93anbi12i 626 . . 3 (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) ↔ (∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔))
95 sbcel1v 3847 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ (𝑦𝑥) ∈ 𝐹)
96 eluni2 4917 . . . 4 ((𝑦𝑥) ∈ 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9795, 96bitri 274 . . 3 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9891, 94, 973imtr4g 295 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) → [(𝑦𝑥) / 𝑥]𝑥 𝐹))
999, 14, 26, 37, 60, 98isfild 23853 1 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  wrex 3060  Vcvv 3462  [wsbc 3776  cun 3945  cin 3946  wss 3947  c0 4325   cuni 4913  cfv 6554  Filcfil 23840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fv 6562  df-fbas 21340  df-fil 23841
This theorem is referenced by:  filssufilg  23906
  Copyright terms: Public domain W3C validator