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

Theorem filuni 22490
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 4804 . . . 4 (𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
2 ssel2 3910 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑓 ∈ (Fil‘𝑋))
3 filelss 22457 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥𝑓) → 𝑥𝑋)
43ex 416 . . . . . . 7 (𝑓 ∈ (Fil‘𝑋) → (𝑥𝑓𝑥𝑋))
52, 4syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (𝑥𝑓𝑥𝑋))
65rexlimdva 3243 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
763ad2ant1 1130 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (∃𝑓𝐹 𝑥𝑓𝑥𝑋))
81, 7syl5bi 245 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹𝑥𝑋))
98pm4.71rd 566 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → (𝑥 𝐹 ↔ (𝑥𝑋𝑥 𝐹)))
10 ssn0 4308 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (Fil‘𝑋) ≠ ∅)
11 fvprc 6638 . . . . 5 𝑋 ∈ V → (Fil‘𝑋) = ∅)
1211necon1ai 3014 . . . 4 ((Fil‘𝑋) ≠ ∅ → 𝑋 ∈ V)
1310, 12syl 17 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → 𝑋 ∈ V)
14133adant3 1129 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 ∈ V)
15 filtop 22460 . . . . . . . . 9 (𝑓 ∈ (Fil‘𝑋) → 𝑋𝑓)
162, 15syl 17 . . . . . . . 8 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → 𝑋𝑓)
1716a1d 25 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑋𝑓))
1817ralimdva 3144 . . . . . 6 (𝐹 ⊆ (Fil‘𝑋) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∀𝑓𝐹 𝑋𝑓))
19 r19.2z 4398 . . . . . . 7 ((𝐹 ≠ ∅ ∧ ∀𝑓𝐹 𝑋𝑓) → ∃𝑓𝐹 𝑋𝑓)
2019ex 416 . . . . . 6 (𝐹 ≠ ∅ → (∀𝑓𝐹 𝑋𝑓 → ∃𝑓𝐹 𝑋𝑓))
2118, 20sylan9 511 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅) → (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → ∃𝑓𝐹 𝑋𝑓))
22213impia 1114 . . . 4 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∃𝑓𝐹 𝑋𝑓)
23 eluni2 4804 . . . 4 (𝑋 𝐹 ↔ ∃𝑓𝐹 𝑋𝑓)
2422, 23sylibr 237 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝑋 𝐹)
25 sbcel1v 3786 . . 3 ([𝑋 / 𝑥]𝑥 𝐹𝑋 𝐹)
2624, 25sylibr 237 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → [𝑋 / 𝑥]𝑥 𝐹)
27 0nelfil 22454 . . . . . 6 (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝑓)
282, 27syl 17 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑓𝐹) → ¬ ∅ ∈ 𝑓)
2928ralrimiva 3149 . . . 4 (𝐹 ⊆ (Fil‘𝑋) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
30293ad2ant1 1130 . . 3 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
31 sbcel1v 3786 . . . . . 6 ([∅ / 𝑥]𝑥 𝐹 ↔ ∅ ∈ 𝐹)
32 eluni2 4804 . . . . . 6 (∅ ∈ 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3331, 32bitri 278 . . . . 5 ([∅ / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 ∅ ∈ 𝑓)
3433notbii 323 . . . 4 [∅ / 𝑥]𝑥 𝐹 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
35 ralnex 3199 . . . 4 (∀𝑓𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃𝑓𝐹 ∅ ∈ 𝑓)
3634, 35bitr4i 281 . . 3 [∅ / 𝑥]𝑥 𝐹 ↔ ∀𝑓𝐹 ¬ ∅ ∈ 𝑓)
3730, 36sylibr 237 . 2 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → ¬ [∅ / 𝑥]𝑥 𝐹)
38 simp13 1202 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
39 r19.29 3216 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑥𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))
4039ex 416 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
4138, 40syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)))
42 simp1 1133 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ⊆ (Fil‘𝑋))
43 simp1 1133 . . . . . . . . 9 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → 𝐹 ⊆ (Fil‘𝑋))
44 simpl 486 . . . . . . . . 9 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓)) → 𝑓𝐹)
4543, 44, 2syl2an 598 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑓 ∈ (Fil‘𝑋))
46 simprrr 781 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑓)
47 simpl2 1189 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑋)
48 simpl3 1190 . . . . . . . 8 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑥𝑦)
49 filss 22458 . . . . . . . 8 ((𝑓 ∈ (Fil‘𝑋) ∧ (𝑥𝑓𝑦𝑋𝑥𝑦)) → 𝑦𝑓)
5045, 46, 47, 48, 49syl13anc 1369 . . . . . . 7 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ (𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓))) → 𝑦𝑓)
5150expr 460 . . . . . 6 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) ∧ 𝑓𝐹) → ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → 𝑦𝑓))
5251reximdva 3233 . . . . 5 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5342, 52syl3an1 1160 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑥𝑓) → ∃𝑓𝐹 𝑦𝑓))
5441, 53syld 47 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → (∃𝑓𝐹 𝑥𝑓 → ∃𝑓𝐹 𝑦𝑓))
55 sbcel1v 3786 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹𝑥 𝐹)
5655, 1bitri 278 . . 3 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑥𝑓)
57 sbcel1v 3786 . . . 4 ([𝑦 / 𝑥]𝑥 𝐹𝑦 𝐹)
58 eluni2 4804 . . . 4 (𝑦 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
5957, 58bitri 278 . . 3 ([𝑦 / 𝑥]𝑥 𝐹 ↔ ∃𝑓𝐹 𝑦𝑓)
6054, 56, 593imtr4g 299 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑦) → ([𝑥 / 𝑥]𝑥 𝐹[𝑦 / 𝑥]𝑥 𝐹))
61 simp13 1202 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹)
62 r19.29 3216 . . . . . 6 ((∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑓𝐹 𝑦𝑓) → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓))
6362ex 416 . . . . 5 (∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
6461, 63syl 17 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (∃𝑓𝐹 𝑦𝑓 → ∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)))
65 simp11 1200 . . . . 5 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → 𝐹 ⊆ (Fil‘𝑋))
66 r19.29 3216 . . . . . . . . . . 11 ((∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔))
6766ex 416 . . . . . . . . . 10 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔)))
68 elun1 4103 . . . . . . . . . . . . . . . 16 (𝑦𝑓𝑦 ∈ (𝑓𝑔))
69 elun2 4104 . . . . . . . . . . . . . . . 16 (𝑥𝑔𝑥 ∈ (𝑓𝑔))
7068, 69anim12i 615 . . . . . . . . . . . . . . 15 ((𝑦𝑓𝑥𝑔) → (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔)))
71 eleq2 2878 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑦𝑦 ∈ (𝑓𝑔)))
72 eleq2 2878 . . . . . . . . . . . . . . . . 17 ( = (𝑓𝑔) → (𝑥𝑥 ∈ (𝑓𝑔)))
7371, 72anbi12d 633 . . . . . . . . . . . . . . . 16 ( = (𝑓𝑔) → ((𝑦𝑥) ↔ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))))
7473rspcev 3571 . . . . . . . . . . . . . . 15 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦 ∈ (𝑓𝑔) ∧ 𝑥 ∈ (𝑓𝑔))) → ∃𝐹 (𝑦𝑥))
7570, 74sylan2 595 . . . . . . . . . . . . . 14 (((𝑓𝑔) ∈ 𝐹 ∧ (𝑦𝑓𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7675an12s 648 . . . . . . . . . . . . 13 ((𝑦𝑓 ∧ ((𝑓𝑔) ∈ 𝐹𝑥𝑔)) → ∃𝐹 (𝑦𝑥))
7776ex 416 . . . . . . . . . . . 12 (𝑦𝑓 → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7877ad2antlr 726 . . . . . . . . . . 11 (((𝑓𝐹𝑦𝑓) ∧ 𝑔𝐹) → (((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
7978rexlimdva 3243 . . . . . . . . . 10 ((𝑓𝐹𝑦𝑓) → (∃𝑔𝐹 ((𝑓𝑔) ∈ 𝐹𝑥𝑔) → ∃𝐹 (𝑦𝑥)))
8067, 79syl9r 78 . . . . . . . . 9 ((𝑓𝐹𝑦𝑓) → (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹 → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥))))
8180impr 458 . . . . . . . 8 ((𝑓𝐹 ∧ (𝑦𝑓 ∧ ∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8281ancom2s 649 . . . . . . 7 ((𝑓𝐹 ∧ (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓)) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8382rexlimiva 3240 . . . . . 6 (∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) → (∃𝑔𝐹 𝑥𝑔 → ∃𝐹 (𝑦𝑥)))
8483imp 410 . . . . 5 ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥))
85 ssel2 3910 . . . . . . 7 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ∈ (Fil‘𝑋))
86 filin 22459 . . . . . . . 8 (( ∈ (Fil‘𝑋) ∧ 𝑦𝑥) → (𝑦𝑥) ∈ )
87863expib 1119 . . . . . . 7 ( ∈ (Fil‘𝑋) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8885, 87syl 17 . . . . . 6 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹) → ((𝑦𝑥) → (𝑦𝑥) ∈ ))
8988reximdva 3233 . . . . 5 (𝐹 ⊆ (Fil‘𝑋) → (∃𝐹 (𝑦𝑥) → ∃𝐹 (𝑦𝑥) ∈ ))
9065, 84, 89syl2im 40 . . . 4 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 (∀𝑔𝐹 (𝑓𝑔) ∈ 𝐹𝑦𝑓) ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
9164, 90syland 605 . . 3 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → ((∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔) → ∃𝐹 (𝑦𝑥) ∈ ))
92 eluni2 4804 . . . . 5 (𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9355, 92bitri 278 . . . 4 ([𝑥 / 𝑥]𝑥 𝐹 ↔ ∃𝑔𝐹 𝑥𝑔)
9459, 93anbi12i 629 . . 3 (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) ↔ (∃𝑓𝐹 𝑦𝑓 ∧ ∃𝑔𝐹 𝑥𝑔))
95 sbcel1v 3786 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ (𝑦𝑥) ∈ 𝐹)
96 eluni2 4804 . . . 4 ((𝑦𝑥) ∈ 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9795, 96bitri 278 . . 3 ([(𝑦𝑥) / 𝑥]𝑥 𝐹 ↔ ∃𝐹 (𝑦𝑥) ∈ )
9891, 94, 973imtr4g 299 . 2 (((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) ∧ 𝑦𝑋𝑥𝑋) → (([𝑦 / 𝑥]𝑥 𝐹[𝑥 / 𝑥]𝑥 𝐹) → [(𝑦𝑥) / 𝑥]𝑥 𝐹))
999, 14, 26, 37, 60, 98isfild 22463 1 ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓𝐹𝑔𝐹 (𝑓𝑔) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2111  wne 2987  wral 3106  wrex 3107  Vcvv 3441  [wsbc 3720  cun 3879  cin 3880  wss 3881  c0 4243   cuni 4800  cfv 6324  Filcfil 22450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fv 6332  df-fbas 20088  df-fil 22451
This theorem is referenced by:  filssufilg  22516
  Copyright terms: Public domain W3C validator