Metamath Proof Explorer

Theorem filuni

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)

Ref Expression
Assertion filuni ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ∪ 𝐹 ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 )
2 ssel2 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
3 filelss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ⊆ 𝑋 )
4 3 ex ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
5 2 4 syl ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
6 5 rexlimdva ⊢ ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) → ( ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
7 6 3ad2ant1 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ( ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋 ) )
8 1 7 biimtrid ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ( 𝑥 ∈ ∪ 𝐹 → 𝑥 ⊆ 𝑋 ) )
9 8 pm4.71rd ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ( 𝑥 ∈ ∪ 𝐹 ↔ ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ∈ ∪ 𝐹 ) ) )
10 ssn0 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ) → ( Fil ‘ 𝑋 ) ≠ ∅ )
11 fvprc ⊢ ( ¬ 𝑋 ∈ V → ( Fil ‘ 𝑋 ) = ∅ )
12 11 necon1ai ⊢ ( ( Fil ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ V )
13 10 12 syl ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ) → 𝑋 ∈ V )
14 13 3adant3 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → 𝑋 ∈ V )
15 filtop ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝑓 )
16 2 15 syl ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → 𝑋 ∈ 𝑓 )
17 16 a1d ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → 𝑋 ∈ 𝑓 ) )
18 17 ralimdva ⊢ ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ∀ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 ) )
19 r19.2z ⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 ) → ∃ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 )
20 19 ex ⊢ ( 𝐹 ≠ ∅ → ( ∀ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 ) )
21 18 20 sylan9 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ) → ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ∃ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 ) )
22 21 3impia ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ∃ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 )
23 eluni2 ⊢ ( 𝑋 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 𝑋 ∈ 𝑓 )
24 22 23 sylibr ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → 𝑋 ∈ ∪ 𝐹 )
25 sbcel1v ⊢ ( [ 𝑋 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ 𝑋 ∈ ∪ 𝐹 )
26 24 25 sylibr ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → [ 𝑋 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 )
27 0nelfil ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝑓 )
28 2 27 syl ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → ¬ ∅ ∈ 𝑓 )
29 28 ralrimiva ⊢ ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) → ∀ 𝑓 ∈ 𝐹 ¬ ∅ ∈ 𝑓 )
30 29 3ad2ant1 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ∀ 𝑓 ∈ 𝐹 ¬ ∅ ∈ 𝑓 )
31 sbcel1v ⊢ ( [ ∅ / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∅ ∈ ∪ 𝐹 )
32 eluni2 ⊢ ( ∅ ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 ∅ ∈ 𝑓 )
33 31 32 bitri ⊢ ( [ ∅ / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 ∅ ∈ 𝑓 )
34 33 notbii ⊢ ( ¬ [ ∅ / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ¬ ∃ 𝑓 ∈ 𝐹 ∅ ∈ 𝑓 )
35 ralnex ⊢ ( ∀ 𝑓 ∈ 𝐹 ¬ ∅ ∈ 𝑓 ↔ ¬ ∃ 𝑓 ∈ 𝐹 ∅ ∈ 𝑓 )
36 34 35 bitr4i ⊢ ( ¬ [ ∅ / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∀ 𝑓 ∈ 𝐹 ¬ ∅ ∈ 𝑓 )
37 30 36 sylibr ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ¬ [ ∅ / 𝑥 ] 𝑥 ∈ ∪ 𝐹 )
38 simp13 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 )
39 r19.29 ⊢ ( ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 ) → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) )
40 39 ex ⊢ ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ( ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) )
41 38 40 syl ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ( ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) )
42 simp1 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → 𝐹 ⊆ ( Fil ‘ 𝑋 ) )
43 simp1 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → 𝐹 ⊆ ( Fil ‘ 𝑋 ) )
44 simpl ⊢ ( ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) → 𝑓 ∈ 𝐹 )
45 43 44 2 syl2an ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
46 simprrr ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) ) → 𝑥 ∈ 𝑓 )
47 simpl2 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) ) → 𝑦 ⊆ 𝑋 )
48 simpl3 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) ) → 𝑥 ⊆ 𝑦 )
49 filss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑓 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ) → 𝑦 ∈ 𝑓 )
50 45 46 47 48 49 syl13anc ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) ) ) → 𝑦 ∈ 𝑓 )
51 50 expr ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) ∧ 𝑓 ∈ 𝐹 ) → ( ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) → 𝑦 ∈ 𝑓 ) )
52 51 reximdva ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ( ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) → ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ) )
53 42 52 syl3an1 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ( ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑓 ) → ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ) )
54 41 53 syld ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ( ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ) )
55 sbcel1v ⊢ ( [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ 𝑥 ∈ ∪ 𝐹 )
56 55 1 bitri ⊢ ( [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 𝑥 ∈ 𝑓 )
57 sbcel1v ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ 𝑦 ∈ ∪ 𝐹 )
58 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 )
59 57 58 bitri ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 )
60 54 56 59 3imtr4g ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑦 ) → ( [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 → [ 𝑦 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ) )
61 simp13 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 )
62 r19.29 ⊢ ( ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ) → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) )
63 62 ex ⊢ ( ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ( ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ) )
64 61 63 syl ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ( ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 → ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ) )
65 simp11 ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ ( Fil ‘ 𝑋 ) )
66 r19.29 ⊢ ( ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 ) → ∃ 𝑔 ∈ 𝐹 ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) )
67 66 ex ⊢ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ( ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 → ∃ 𝑔 ∈ 𝐹 ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) ) )
68 elun1 ⊢ ( 𝑦 ∈ 𝑓 → 𝑦 ∈ ( 𝑓 ∪ 𝑔 ) )
69 elun2 ⊢ ( 𝑥 ∈ 𝑔 → 𝑥 ∈ ( 𝑓 ∪ 𝑔 ) )
70 68 69 anim12i ⊢ ( ( 𝑦 ∈ 𝑓 ∧ 𝑥 ∈ 𝑔 ) → ( 𝑦 ∈ ( 𝑓 ∪ 𝑔 ) ∧ 𝑥 ∈ ( 𝑓 ∪ 𝑔 ) ) )
71 eleq2 ⊢ ( ℎ = ( 𝑓 ∪ 𝑔 ) → ( 𝑦 ∈ ℎ ↔ 𝑦 ∈ ( 𝑓 ∪ 𝑔 ) ) )
72 eleq2 ⊢ ( ℎ = ( 𝑓 ∪ 𝑔 ) → ( 𝑥 ∈ ℎ ↔ 𝑥 ∈ ( 𝑓 ∪ 𝑔 ) ) )
73 71 72 anbi12d ⊢ ( ℎ = ( 𝑓 ∪ 𝑔 ) → ( ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ↔ ( 𝑦 ∈ ( 𝑓 ∪ 𝑔 ) ∧ 𝑥 ∈ ( 𝑓 ∪ 𝑔 ) ) ) )
74 73 rspcev ⊢ ( ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ ( 𝑦 ∈ ( 𝑓 ∪ 𝑔 ) ∧ 𝑥 ∈ ( 𝑓 ∪ 𝑔 ) ) ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) )
75 70 74 sylan2 ⊢ ( ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ ( 𝑦 ∈ 𝑓 ∧ 𝑥 ∈ 𝑔 ) ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) )
76 75 an12s ⊢ ( ( 𝑦 ∈ 𝑓 ∧ ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) )
77 76 ex ⊢ ( 𝑦 ∈ 𝑓 → ( ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
78 77 ad2antlr ⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ∧ 𝑔 ∈ 𝐹 ) → ( ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
79 78 rexlimdva ⊢ ( ( 𝑓 ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) → ( ∃ 𝑔 ∈ 𝐹 ( ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
80 67 79 syl9r ⊢ ( ( 𝑓 ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) → ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 → ( ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) ) )
81 80 impr ⊢ ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑦 ∈ 𝑓 ∧ ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ) → ( ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
82 81 ancom2s ⊢ ( ( 𝑓 ∈ 𝐹 ∧ ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ) → ( ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
83 82 rexlimiva ⊢ ( ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) → ( ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) ) )
84 83 imp ⊢ ( ( ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ∧ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) )
85 ssel2 ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ ℎ ∈ 𝐹 ) → ℎ ∈ ( Fil ‘ 𝑋 ) )
86 filin ⊢ ( ( ℎ ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) → ( 𝑦 ∩ 𝑥 ) ∈ ℎ )
87 86 3expib ⊢ ( ℎ ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) → ( 𝑦 ∩ 𝑥 ) ∈ ℎ ) )
88 85 87 syl ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ ℎ ∈ 𝐹 ) → ( ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) → ( 𝑦 ∩ 𝑥 ) ∈ ℎ ) )
89 88 reximdva ⊢ ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) → ( ∃ ℎ ∈ 𝐹 ( 𝑦 ∈ ℎ ∧ 𝑥 ∈ ℎ ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ∈ ℎ ) )
90 65 84 89 syl2im ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ( ( ∃ 𝑓 ∈ 𝐹 ( ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ∧ 𝑦 ∈ 𝑓 ) ∧ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ∈ ℎ ) )
91 64 90 syland ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ( ( ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ∧ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 ) → ∃ ℎ ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ∈ ℎ ) )
92 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 )
93 55 92 bitri ⊢ ( [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 )
94 59 93 anbi12i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ∧ [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ) ↔ ( ∃ 𝑓 ∈ 𝐹 𝑦 ∈ 𝑓 ∧ ∃ 𝑔 ∈ 𝐹 𝑥 ∈ 𝑔 ) )
95 sbcel1v ⊢ ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ( 𝑦 ∩ 𝑥 ) ∈ ∪ 𝐹 )
96 eluni2 ⊢ ( ( 𝑦 ∩ 𝑥 ) ∈ ∪ 𝐹 ↔ ∃ ℎ ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ∈ ℎ )
97 95 96 bitri ⊢ ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ↔ ∃ ℎ ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ∈ ℎ )
98 91 94 97 3imtr4g ⊢ ( ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) → ( ( [ 𝑦 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ∧ [ 𝑥 / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ) → [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 ∈ ∪ 𝐹 ) )
99 9 14 26 37 60 98 isfild ⊢ ( ( 𝐹 ⊆ ( Fil ‘ 𝑋 ) ∧ 𝐹 ≠ ∅ ∧ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ 𝐹 ( 𝑓 ∪ 𝑔 ) ∈ 𝐹 ) → ∪ 𝐹 ∈ ( Fil ‘ 𝑋 ) )