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

Theorem filuni 21736
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 4472 . . . 4 (𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
2 ssel2 3631 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓 ∈ (Fil‘𝑋))
3 filelss 21703 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
43ex 449 . . . . . . 7 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
52, 4syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (𝑥𝑓𝑥𝑋))
65rexlimdva 3060 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
763ad2ant1 1102 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
81, 7syl5bi 232 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹𝑥𝑋))
98pm4.71rd 668 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹 ↔ (𝑥𝑋𝑥 𝐹)))
10 ssn0 4009 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (Fil‘𝑋) ≠ ∅)
11 fvprc 6223 . . . . 5 𝑋 ∈ V → (Fil‘𝑋) = ∅)
1211necon1ai 2850 . . . 4 ((Fil‘𝑋) ≠ ∅ → 𝑋 ∈ V)
1310, 12syl 17 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → 𝑋 ∈ V)
14133adant3 1101 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 ∈ V)
15 filtop 21706 . . . . . . . . 9 (𝑓 ∈ (Fil‘𝑋) → 𝑋𝑓)
162, 15syl 17 . . . . . . . 8 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑋𝑓)
1716a1d 25 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑋𝑓))
1817ralimdva 2991 . . . . . 6 (𝐹 ⊆ (Fil‘𝑋) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∀𝑓𝐹 𝑋𝑓))
19 r19.2z 4093 . . . . . . 7 ((𝐹 ≠ ∅ ∧ ∀𝑓𝐹 𝑋𝑓) → ∃𝑓𝐹 𝑋𝑓)
2019ex 449 . . . . . 6 (𝐹 ≠ ∅ → (∀𝑓𝐹 𝑋𝑓 → ∃𝑓𝐹 𝑋𝑓))
2118, 20sylan9 690 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∃𝑓𝐹 𝑋𝑓))
22213impia 1280 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∃𝑓𝐹 𝑋𝑓)
23 eluni2 4472 . . . 4 (𝑋 𝐹 ↔ ∃𝑓𝐹 𝑋𝑓)
2422, 23sylibr 224 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 𝐹)
25 sbcel1v 3528 . . 3 ([𝑋 / 𝑥]𝑥 𝐹𝑋 𝐹)
2624, 25sylibr 224 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → [𝑋 / 𝑥]𝑥 𝐹)
27 0nelfil 21700 . . . . . 6 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
282, 27syl 17 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → ¬ ∅ ∈ 𝑓)
2928ralrimiva 2995 . . . 4 (𝐹 ⊆ (Fil‘𝑋) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
30293ad2ant1 1102 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
31 sbcel1v 3528 . . . . . 6 ([∅ / 𝑥]𝑥 𝐹 ↔ ∅ ∈ 𝐹)
32 eluni2 4472 . . . . . 6 (∅ ∈ 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3331, 32bitri 264 . . . . 5 ([∅ / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3433notbii 309 . . . 4 [∅ / 𝑥]𝑥 𝐹 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
35 ralnex 3021 . . . 4 (∀𝑓𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
3634, 35bitr4i 267 . . 3 [∅ / 𝑥]𝑥 𝐹 ↔ ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
3730, 36sylibr 224 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ¬ [∅ / 𝑥]𝑥 𝐹)
38 simp13 1113 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
39 r19.29 3101 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑥𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))
4039ex 449 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
4138, 40syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
42 simp1 1081 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ⊆ (Fil‘𝑋))
43 simp1 1081 . . . . . . . . 9 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → 𝐹 ⊆ (Fil‘𝑋))
44 simpl 472 . . . . . . . . 9 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)) → 𝑓𝐹)
4543, 44, 2syl2an 493 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑓 ∈ (Fil‘𝑋))
46 simprrr 822 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑓)
47 simpl2 1085 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑋)
48 simpl3 1086 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑦)
49 filss 21704 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ (𝑥𝑓𝑦𝑋𝑥𝑦)) → 𝑦𝑓)
5045, 46, 47, 48, 49syl13anc 1368 . . . . . . 7 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑓)
5150expr 642 . . . . . 6 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ 𝑓𝐹) → ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → 𝑦𝑓))
5251reximdva 3046 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5342, 52syl3an1 1399 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5441, 53syld 47 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 𝑦𝑓))
55 sbcel1v 3528 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹𝑥 𝐹)
5655, 1bitri 264 . . 3 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
57 sbcel1v 3528 . . . 4 ([𝑦 / 𝑥]𝑥 𝐹𝑦 𝐹)
58 eluni2 4472 . . . 4 (𝑦 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
5957, 58bitri 264 . . 3 ([𝑦 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
6054, 56, 593imtr4g 285 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ([𝑥 / 𝑥]𝑥 𝐹[𝑦 / 𝑥]𝑥 𝐹))
61 simp13 1113 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
62 r19.29 3101 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑦𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓))
6362ex 449 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
6461, 63syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
65 simp11 1111 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → 𝐹 ⊆ (Fil‘𝑋))
66 r19.29 3101 . . . . . . . . . . 11 ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔))
6766ex 449 . . . . . . . . . 10 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔)))
68 elun1 3813 . . . . . . . . . . . . . . . 16 (𝑦𝑓𝑦 ∈ (𝑓𝑔))
69 elun2 3814 . . . . . . . . . . . . . . . 16 (𝑥𝑔𝑥 ∈ (𝑓𝑔))
7068, 69anim12i 589 . . . . . . . . . . . . . . 15 ((𝑦𝑓𝑥𝑔) → (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔)))
71 eleq2 2719 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑦𝑦 ∈ (𝑓𝑔)))
72 eleq2 2719 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑥𝑥 ∈ (𝑓𝑔)))
7371, 72anbi12d 747 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑔) → ((𝑦𝑥) ↔ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))))
7473rspcev 3340 . . . . . . . . . . . . . . 15 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))) → ∃𝐹 (𝑦𝑥))
7570, 74sylan2 490 . . . . . . . . . . . . . 14 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦𝑓𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7675an12s 860 . . . . . . . . . . . . 13 ((𝑦𝑓 ∧ ((𝑓𝑔) ∈ 𝐹𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7776ex 449 . . . . . . . . . . . 12 (𝑦𝑓 → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7877ad2antlr 763 . . . . . . . . . . 11 (((𝑓𝐹𝑦𝑓) ∧ 𝑔𝐹) → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7978rexlimdva 3060 . . . . . . . . . 10 ((𝑓𝐹𝑦𝑓) → (∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
8067, 79syl9r 78 . . . . . . . . 9 ((𝑓𝐹𝑦𝑓) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥))))
8180impr 648 . . . . . . . 8 ((𝑓𝐹 ∧ (𝑦𝑓 ∧ ∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8281ancom2s 861 . . . . . . 7 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8382rexlimiva 3057 . . . . . 6 (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8483imp 444 . . . . 5 ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥))
85 ssel2 3631 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ∈ (Fil‘𝑋))
86 filin 21705 . . . . . . . 8 (( ∈ (Fil‘𝑋) ∧ 𝑦𝑥) → (𝑦𝑥) ∈ )
87863expib 1287 . . . . . . 7 ( ∈ (Fil‘𝑋) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8885, 87syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8988reximdva 3046 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝐹 (𝑦𝑥) → ∃𝐹 (𝑦𝑥) ∈ ))
9065, 84, 89syl2im 40 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
9164, 90syland 497 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
92 eluni2 4472 . . . . 5 (𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9355, 92bitri 264 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9459, 93anbi12i 733 . . 3 (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) ↔ (∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔))
95 sbcel1v 3528 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ (𝑦𝑥) ∈ 𝐹)
96 eluni2 4472 . . . 4 ((𝑦𝑥) ∈ 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9795, 96bitri 264 . . 3 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9891, 94, 973imtr4g 285 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) → [(𝑦𝑥) / 𝑥]𝑥 𝐹))
999, 14, 26, 37, 60, 98isfild 21709 1 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  [wsbc 3468  cun 3605  cin 3606  wss 3607  c0 3948   cuni 4468  cfv 5926  Filcfil 21696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fv 5934  df-fbas 19791  df-fil 21697
This theorem is referenced by:  filssufilg  21762
  Copyright terms: Public domain W3C validator