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

Theorem filuni 21499
 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 4376 . . . 4 (𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
2 ssel2 3563 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓 ∈ (Fil‘𝑋))
3 filelss 21466 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
43ex 449 . . . . . . 7 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
52, 4syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (𝑥𝑓𝑥𝑋))
65rexlimdva 3013 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
763ad2ant1 1075 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
81, 7syl5bi 231 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹𝑥𝑋))
98pm4.71rd 665 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹 ↔ (𝑥𝑋𝑥 𝐹)))
10 ssn0 3928 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (Fil‘𝑋) ≠ ∅)
11 fvprc 6097 . . . . 5 𝑋 ∈ V → (Fil‘𝑋) = ∅)
1211necon1ai 2809 . . . 4 ((Fil‘𝑋) ≠ ∅ → 𝑋 ∈ V)
1310, 12syl 17 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → 𝑋 ∈ V)
14133adant3 1074 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 ∈ V)
15 filtop 21469 . . . . . . . . 9 (𝑓 ∈ (Fil‘𝑋) → 𝑋𝑓)
162, 15syl 17 . . . . . . . 8 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑋𝑓)
1716a1d 25 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑋𝑓))
1817ralimdva 2945 . . . . . 6 (𝐹 ⊆ (Fil‘𝑋) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∀𝑓𝐹 𝑋𝑓))
19 r19.2z 4012 . . . . . . 7 ((𝐹 ≠ ∅ ∧ ∀𝑓𝐹 𝑋𝑓) → ∃𝑓𝐹 𝑋𝑓)
2019ex 449 . . . . . 6 (𝐹 ≠ ∅ → (∀𝑓𝐹 𝑋𝑓 → ∃𝑓𝐹 𝑋𝑓))
2118, 20sylan9 687 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∃𝑓𝐹 𝑋𝑓))
22213impia 1253 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∃𝑓𝐹 𝑋𝑓)
23 eluni2 4376 . . . 4 (𝑋 𝐹 ↔ ∃𝑓𝐹 𝑋𝑓)
2422, 23sylibr 223 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 𝐹)
25 sbcel1v 3462 . . 3 ([𝑋 / 𝑥]𝑥 𝐹𝑋 𝐹)
2624, 25sylibr 223 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → [𝑋 / 𝑥]𝑥 𝐹)
27 0nelfil 21463 . . . . . 6 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
282, 27syl 17 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → ¬ ∅ ∈ 𝑓)
2928ralrimiva 2949 . . . 4 (𝐹 ⊆ (Fil‘𝑋) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
30293ad2ant1 1075 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
31 sbcel1v 3462 . . . . . 6 ([∅ / 𝑥]𝑥 𝐹 ↔ ∅ ∈ 𝐹)
32 eluni2 4376 . . . . . 6 (∅ ∈ 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3331, 32bitri 263 . . . . 5 ([∅ / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3433notbii 309 . . . 4 [∅ / 𝑥]𝑥 𝐹 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
35 ralnex 2975 . . . 4 (∀𝑓𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
3634, 35bitr4i 266 . . 3 [∅ / 𝑥]𝑥 𝐹 ↔ ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
3730, 36sylibr 223 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ¬ [∅ / 𝑥]𝑥 𝐹)
38 simp13 1086 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
39 r19.29 3054 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑥𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))
4039ex 449 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
4138, 40syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
42 simp1 1054 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ⊆ (Fil‘𝑋))
43 simp1 1054 . . . . . . . . 9 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → 𝐹 ⊆ (Fil‘𝑋))
44 simpl 472 . . . . . . . . 9 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)) → 𝑓𝐹)
4543, 44, 2syl2an 493 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑓 ∈ (Fil‘𝑋))
46 simprrr 801 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑓)
47 simpl2 1058 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑋)
48 simpl3 1059 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑦)
49 filss 21467 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ (𝑥𝑓𝑦𝑋𝑥𝑦)) → 𝑦𝑓)
5045, 46, 47, 48, 49syl13anc 1320 . . . . . . 7 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑓)
5150expr 641 . . . . . 6 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ 𝑓𝐹) → ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → 𝑦𝑓))
5251reximdva 3000 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5342, 52syl3an1 1351 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5441, 53syld 46 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 𝑦𝑓))
55 sbcel1v 3462 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹𝑥 𝐹)
5655, 1bitri 263 . . 3 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
57 sbcel1v 3462 . . . 4 ([𝑦 / 𝑥]𝑥 𝐹𝑦 𝐹)
58 eluni2 4376 . . . 4 (𝑦 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
5957, 58bitri 263 . . 3 ([𝑦 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
6054, 56, 593imtr4g 284 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ([𝑥 / 𝑥]𝑥 𝐹[𝑦 / 𝑥]𝑥 𝐹))
61 simp13 1086 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
62 r19.29 3054 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑦𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓))
6362ex 449 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
6461, 63syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
65 simp11 1084 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → 𝐹 ⊆ (Fil‘𝑋))
66 r19.29 3054 . . . . . . . . . . 11 ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔))
6766ex 449 . . . . . . . . . 10 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔)))
68 elun1 3742 . . . . . . . . . . . . . . . 16 (𝑦𝑓𝑦 ∈ (𝑓𝑔))
69 elun2 3743 . . . . . . . . . . . . . . . 16 (𝑥𝑔𝑥 ∈ (𝑓𝑔))
7068, 69anim12i 588 . . . . . . . . . . . . . . 15 ((𝑦𝑓𝑥𝑔) → (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔)))
71 eleq2 2677 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑦𝑦 ∈ (𝑓𝑔)))
72 eleq2 2677 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑥𝑥 ∈ (𝑓𝑔)))
7371, 72anbi12d 743 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑔) → ((𝑦𝑥) ↔ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))))
7473rspcev 3282 . . . . . . . . . . . . . . 15 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))) → ∃𝐹 (𝑦𝑥))
7570, 74sylan2 490 . . . . . . . . . . . . . 14 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦𝑓𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7675an12s 839 . . . . . . . . . . . . 13 ((𝑦𝑓 ∧ ((𝑓𝑔) ∈ 𝐹𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7776ex 449 . . . . . . . . . . . 12 (𝑦𝑓 → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7877ad2antlr 759 . . . . . . . . . . 11 (((𝑓𝐹𝑦𝑓) ∧ 𝑔𝐹) → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7978rexlimdva 3013 . . . . . . . . . 10 ((𝑓𝐹𝑦𝑓) → (∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
8067, 79syl9r 76 . . . . . . . . 9 ((𝑓𝐹𝑦𝑓) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥))))
8180impr 647 . . . . . . . 8 ((𝑓𝐹 ∧ (𝑦𝑓 ∧ ∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8281ancom2s 840 . . . . . . 7 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8382rexlimiva 3010 . . . . . 6 (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8483imp 444 . . . . 5 ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥))
85 ssel2 3563 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ∈ (Fil‘𝑋))
86 filin 21468 . . . . . . . 8 (( ∈ (Fil‘𝑋) ∧ 𝑦𝑥) → (𝑦𝑥) ∈ )
87863expib 1260 . . . . . . 7 ( ∈ (Fil‘𝑋) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8885, 87syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8988reximdva 3000 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝐹 (𝑦𝑥) → ∃𝐹 (𝑦𝑥) ∈ ))
9065, 84, 89syl2im 39 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
9164, 90syland 497 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
92 eluni2 4376 . . . . 5 (𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9355, 92bitri 263 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9459, 93anbi12i 729 . . 3 (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) ↔ (∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔))
95 sbcel1v 3462 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ (𝑦𝑥) ∈ 𝐹)
96 eluni2 4376 . . . 4 ((𝑦𝑥) ∈ 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9795, 96bitri 263 . . 3 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9891, 94, 973imtr4g 284 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) → [(𝑦𝑥) / 𝑥]𝑥 𝐹))
999, 14, 26, 37, 60, 98isfild 21472 1 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173  [wsbc 3402   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372  ‘cfv 5804  Filcfil 21459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812  df-fbas 19564  df-fil 21460 This theorem is referenced by:  filssufilg  21525
 Copyright terms: Public domain W3C validator