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

Theorem filuni 23142
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 4856 . . . 4 (𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
2 ssel2 3927 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓 ∈ (Fil‘𝑋))
3 filelss 23109 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
43ex 413 . . . . . . 7 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
52, 4syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (𝑥𝑓𝑥𝑋))
65rexlimdva 3148 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
763ad2ant1 1132 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
81, 7biimtrid 241 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹𝑥𝑋))
98pm4.71rd 563 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹 ↔ (𝑥𝑋𝑥 𝐹)))
10 ssn0 4347 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (Fil‘𝑋) ≠ ∅)
11 fvprc 6817 . . . . 5 𝑋 ∈ V → (Fil‘𝑋) = ∅)
1211necon1ai 2968 . . . 4 ((Fil‘𝑋) ≠ ∅ → 𝑋 ∈ V)
1310, 12syl 17 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → 𝑋 ∈ V)
14133adant3 1131 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 ∈ V)
15 filtop 23112 . . . . . . . . 9 (𝑓 ∈ (Fil‘𝑋) → 𝑋𝑓)
162, 15syl 17 . . . . . . . 8 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑋𝑓)
1716a1d 25 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑋𝑓))
1817ralimdva 3160 . . . . . 6 (𝐹 ⊆ (Fil‘𝑋) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∀𝑓𝐹 𝑋𝑓))
19 r19.2z 4439 . . . . . . 7 ((𝐹 ≠ ∅ ∧ ∀𝑓𝐹 𝑋𝑓) → ∃𝑓𝐹 𝑋𝑓)
2019ex 413 . . . . . 6 (𝐹 ≠ ∅ → (∀𝑓𝐹 𝑋𝑓 → ∃𝑓𝐹 𝑋𝑓))
2118, 20sylan9 508 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∃𝑓𝐹 𝑋𝑓))
22213impia 1116 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∃𝑓𝐹 𝑋𝑓)
23 eluni2 4856 . . . 4 (𝑋 𝐹 ↔ ∃𝑓𝐹 𝑋𝑓)
2422, 23sylibr 233 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 𝐹)
25 sbcel1v 3798 . . 3 ([𝑋 / 𝑥]𝑥 𝐹𝑋 𝐹)
2624, 25sylibr 233 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → [𝑋 / 𝑥]𝑥 𝐹)
27 0nelfil 23106 . . . . . 6 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
282, 27syl 17 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → ¬ ∅ ∈ 𝑓)
2928ralrimiva 3139 . . . 4 (𝐹 ⊆ (Fil‘𝑋) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
30293ad2ant1 1132 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
31 sbcel1v 3798 . . . . . 6 ([∅ / 𝑥]𝑥 𝐹 ↔ ∅ ∈ 𝐹)
32 eluni2 4856 . . . . . 6 (∅ ∈ 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3331, 32bitri 274 . . . . 5 ([∅ / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3433notbii 319 . . . 4 [∅ / 𝑥]𝑥 𝐹 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
35 ralnex 3072 . . . 4 (∀𝑓𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
3634, 35bitr4i 277 . . 3 [∅ / 𝑥]𝑥 𝐹 ↔ ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
3730, 36sylibr 233 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ¬ [∅ / 𝑥]𝑥 𝐹)
38 simp13 1204 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
39 r19.29 3113 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑥𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))
4039ex 413 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
4138, 40syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
42 simp1 1135 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ⊆ (Fil‘𝑋))
43 simp1 1135 . . . . . . . . 9 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → 𝐹 ⊆ (Fil‘𝑋))
44 simpl 483 . . . . . . . . 9 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)) → 𝑓𝐹)
4543, 44, 2syl2an 596 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑓 ∈ (Fil‘𝑋))
46 simprrr 779 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑓)
47 simpl2 1191 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑋)
48 simpl3 1192 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑦)
49 filss 23110 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ (𝑥𝑓𝑦𝑋𝑥𝑦)) → 𝑦𝑓)
5045, 46, 47, 48, 49syl13anc 1371 . . . . . . 7 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑓)
5150expr 457 . . . . . 6 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ 𝑓𝐹) → ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → 𝑦𝑓))
5251reximdva 3161 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5342, 52syl3an1 1162 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5441, 53syld 47 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 𝑦𝑓))
55 sbcel1v 3798 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹𝑥 𝐹)
5655, 1bitri 274 . . 3 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
57 sbcel1v 3798 . . . 4 ([𝑦 / 𝑥]𝑥 𝐹𝑦 𝐹)
58 eluni2 4856 . . . 4 (𝑦 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
5957, 58bitri 274 . . 3 ([𝑦 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
6054, 56, 593imtr4g 295 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ([𝑥 / 𝑥]𝑥 𝐹[𝑦 / 𝑥]𝑥 𝐹))
61 simp13 1204 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
62 r19.29 3113 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑦𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓))
6362ex 413 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
6461, 63syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
65 simp11 1202 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → 𝐹 ⊆ (Fil‘𝑋))
66 r19.29 3113 . . . . . . . . . . 11 ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔))
6766ex 413 . . . . . . . . . 10 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔)))
68 elun1 4123 . . . . . . . . . . . . . . . 16 (𝑦𝑓𝑦 ∈ (𝑓𝑔))
69 elun2 4124 . . . . . . . . . . . . . . . 16 (𝑥𝑔𝑥 ∈ (𝑓𝑔))
7068, 69anim12i 613 . . . . . . . . . . . . . . 15 ((𝑦𝑓𝑥𝑔) → (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔)))
71 eleq2 2825 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑦𝑦 ∈ (𝑓𝑔)))
72 eleq2 2825 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑥𝑥 ∈ (𝑓𝑔)))
7371, 72anbi12d 631 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑔) → ((𝑦𝑥) ↔ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))))
7473rspcev 3570 . . . . . . . . . . . . . . 15 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))) → ∃𝐹 (𝑦𝑥))
7570, 74sylan2 593 . . . . . . . . . . . . . 14 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦𝑓𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7675an12s 646 . . . . . . . . . . . . 13 ((𝑦𝑓 ∧ ((𝑓𝑔) ∈ 𝐹𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7776ex 413 . . . . . . . . . . . 12 (𝑦𝑓 → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7877ad2antlr 724 . . . . . . . . . . 11 (((𝑓𝐹𝑦𝑓) ∧ 𝑔𝐹) → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7978rexlimdva 3148 . . . . . . . . . 10 ((𝑓𝐹𝑦𝑓) → (∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
8067, 79syl9r 78 . . . . . . . . 9 ((𝑓𝐹𝑦𝑓) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥))))
8180impr 455 . . . . . . . 8 ((𝑓𝐹 ∧ (𝑦𝑓 ∧ ∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8281ancom2s 647 . . . . . . 7 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8382rexlimiva 3140 . . . . . 6 (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8483imp 407 . . . . 5 ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥))
85 ssel2 3927 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ∈ (Fil‘𝑋))
86 filin 23111 . . . . . . . 8 (( ∈ (Fil‘𝑋) ∧ 𝑦𝑥) → (𝑦𝑥) ∈ )
87863expib 1121 . . . . . . 7 ( ∈ (Fil‘𝑋) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8885, 87syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8988reximdva 3161 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝐹 (𝑦𝑥) → ∃𝐹 (𝑦𝑥) ∈ ))
9065, 84, 89syl2im 40 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
9164, 90syland 603 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
92 eluni2 4856 . . . . 5 (𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9355, 92bitri 274 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9459, 93anbi12i 627 . . 3 (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) ↔ (∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔))
95 sbcel1v 3798 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ (𝑦𝑥) ∈ 𝐹)
96 eluni2 4856 . . . 4 ((𝑦𝑥) ∈ 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9795, 96bitri 274 . . 3 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9891, 94, 973imtr4g 295 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) → [(𝑦𝑥) / 𝑥]𝑥 𝐹))
999, 14, 26, 37, 60, 98isfild 23115 1 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441  [wsbc 3727  cun 3896  cin 3897  wss 3898  c0 4269   cuni 4852  cfv 6479  Filcfil 23102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fv 6487  df-fbas 20700  df-fil 23103
This theorem is referenced by:  filssufilg  23168
  Copyright terms: Public domain W3C validator