Metamath Proof Explorer


Theorem fbssfi

Description: A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbssfi ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥𝐹 𝑥𝐴 )

Proof

Step Hyp Ref Expression
1 dffi2 ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } )
2 sseq2 ( 𝑡 = ( 𝑢𝑣 ) → ( 𝑥𝑡𝑥 ⊆ ( 𝑢𝑣 ) ) )
3 2 rexbidv ( 𝑡 = ( 𝑢𝑣 ) → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑢𝑣 ) ) )
4 inss1 ( 𝑢𝑣 ) ⊆ 𝑢
5 simp1r ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → 𝑢 ∈ 𝒫 𝐹 )
6 5 elpwid ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → 𝑢 𝐹 )
7 4 6 sstrid ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑢𝑣 ) ⊆ 𝐹 )
8 vex 𝑢 ∈ V
9 8 inex1 ( 𝑢𝑣 ) ∈ V
10 9 elpw ( ( 𝑢𝑣 ) ∈ 𝒫 𝐹 ↔ ( 𝑢𝑣 ) ⊆ 𝐹 )
11 7 10 sylibr ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑢𝑣 ) ∈ 𝒫 𝐹 )
12 simpl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
13 simpl ( ( 𝑦𝐹𝑦𝑢 ) → 𝑦𝐹 )
14 simpl ( ( 𝑧𝐹𝑧𝑣 ) → 𝑧𝐹 )
15 fbasssin ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦𝐹𝑧𝐹 ) → ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑦𝑧 ) )
16 12 13 14 15 syl3an ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑦𝑧 ) )
17 ss2in ( ( 𝑦𝑢𝑧𝑣 ) → ( 𝑦𝑧 ) ⊆ ( 𝑢𝑣 ) )
18 17 ad2ant2l ( ( ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑦𝑧 ) ⊆ ( 𝑢𝑣 ) )
19 18 3adant1 ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑦𝑧 ) ⊆ ( 𝑢𝑣 ) )
20 sstr ( ( 𝑥 ⊆ ( 𝑦𝑧 ) ∧ ( 𝑦𝑧 ) ⊆ ( 𝑢𝑣 ) ) → 𝑥 ⊆ ( 𝑢𝑣 ) )
21 20 expcom ( ( 𝑦𝑧 ) ⊆ ( 𝑢𝑣 ) → ( 𝑥 ⊆ ( 𝑦𝑧 ) → 𝑥 ⊆ ( 𝑢𝑣 ) ) )
22 19 21 syl ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑥 ⊆ ( 𝑦𝑧 ) → 𝑥 ⊆ ( 𝑢𝑣 ) ) )
23 22 reximdv ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑦𝑧 ) → ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑢𝑣 ) ) )
24 16 23 mpd ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ∃ 𝑥𝐹 𝑥 ⊆ ( 𝑢𝑣 ) )
25 3 11 24 elrabd ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
26 25 3expa ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ) ∧ ( 𝑧𝐹𝑧𝑣 ) ) → ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
27 26 rexlimdvaa ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ) → ( ∃ 𝑧𝐹 𝑧𝑣 → ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
28 27 ralrimivw ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ) → ∀ 𝑣 ∈ 𝒫 𝐹 ( ∃ 𝑧𝐹 𝑧𝑣 → ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
29 sseq2 ( 𝑡 = 𝑣 → ( 𝑥𝑡𝑥𝑣 ) )
30 29 rexbidv ( 𝑡 = 𝑣 → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑥𝐹 𝑥𝑣 ) )
31 sseq1 ( 𝑥 = 𝑧 → ( 𝑥𝑣𝑧𝑣 ) )
32 31 cbvrexvw ( ∃ 𝑥𝐹 𝑥𝑣 ↔ ∃ 𝑧𝐹 𝑧𝑣 )
33 30 32 bitrdi ( 𝑡 = 𝑣 → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑧𝐹 𝑧𝑣 ) )
34 33 ralrab ( ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ↔ ∀ 𝑣 ∈ 𝒫 𝐹 ( ∃ 𝑧𝐹 𝑧𝑣 → ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
35 28 34 sylibr ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) ∧ ( 𝑦𝐹𝑦𝑢 ) ) → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
36 35 rexlimdvaa ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 𝐹 ) → ( ∃ 𝑦𝐹 𝑦𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
37 36 ralrimiva ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ 𝒫 𝐹 ( ∃ 𝑦𝐹 𝑦𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
38 sseq2 ( 𝑡 = 𝑢 → ( 𝑥𝑡𝑥𝑢 ) )
39 38 rexbidv ( 𝑡 = 𝑢 → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑥𝐹 𝑥𝑢 ) )
40 sseq1 ( 𝑥 = 𝑦 → ( 𝑥𝑢𝑦𝑢 ) )
41 40 cbvrexvw ( ∃ 𝑥𝐹 𝑥𝑢 ↔ ∃ 𝑦𝐹 𝑦𝑢 )
42 39 41 bitrdi ( 𝑡 = 𝑢 → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑦𝐹 𝑦𝑢 ) )
43 42 ralrab ( ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ↔ ∀ 𝑢 ∈ 𝒫 𝐹 ( ∃ 𝑦𝐹 𝑦𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
44 37 43 sylibr ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
45 pwuni 𝐹 ⊆ 𝒫 𝐹
46 ssid 𝑡𝑡
47 sseq1 ( 𝑥 = 𝑡 → ( 𝑥𝑡𝑡𝑡 ) )
48 47 rspcev ( ( 𝑡𝐹𝑡𝑡 ) → ∃ 𝑥𝐹 𝑥𝑡 )
49 46 48 mpan2 ( 𝑡𝐹 → ∃ 𝑥𝐹 𝑥𝑡 )
50 49 rgen 𝑡𝐹𝑥𝐹 𝑥𝑡
51 ssrab ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ↔ ( 𝐹 ⊆ 𝒫 𝐹 ∧ ∀ 𝑡𝐹𝑥𝐹 𝑥𝑡 ) )
52 45 50 51 mpbir2an 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 }
53 44 52 jctil ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
54 uniexg ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ∈ V )
55 pwexg ( 𝐹 ∈ V → 𝒫 𝐹 ∈ V )
56 rabexg ( 𝒫 𝐹 ∈ V → { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ V )
57 sseq2 ( 𝑧 = { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ( 𝐹𝑧𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
58 eleq2 ( 𝑧 = { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ( ( 𝑢𝑣 ) ∈ 𝑧 ↔ ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
59 58 raleqbi1dv ( 𝑧 = { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ( ∀ 𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ↔ ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
60 59 raleqbi1dv ( 𝑧 = { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ( ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ↔ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) )
61 57 60 anbi12d ( 𝑧 = { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ( ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) ) )
62 61 elabg ( { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ V → ( { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) ) )
63 54 55 56 62 4syl ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ( 𝑢𝑣 ) ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ) ) )
64 53 63 mpbird ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } )
65 intss1 ( { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ∈ { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } → { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
66 64 65 syl ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑧 ∣ ( 𝐹𝑧 ∧ ∀ 𝑢𝑧𝑣𝑧 ( 𝑢𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
67 1 66 eqsstrd ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) ⊆ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
68 67 sselda ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → 𝐴 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } )
69 sseq2 ( 𝑡 = 𝐴 → ( 𝑥𝑡𝑥𝐴 ) )
70 69 rexbidv ( 𝑡 = 𝐴 → ( ∃ 𝑥𝐹 𝑥𝑡 ↔ ∃ 𝑥𝐹 𝑥𝐴 ) )
71 70 elrab ( 𝐴 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } ↔ ( 𝐴 ∈ 𝒫 𝐹 ∧ ∃ 𝑥𝐹 𝑥𝐴 ) )
72 71 simprbi ( 𝐴 ∈ { 𝑡 ∈ 𝒫 𝐹 ∣ ∃ 𝑥𝐹 𝑥𝑡 } → ∃ 𝑥𝐹 𝑥𝐴 )
73 68 72 syl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥𝐹 𝑥𝐴 )