Metamath Proof Explorer

Theorem tsmsfbas

Description: The collection of all sets of the form F ( z ) = { y e. S | z C_ y } , which can be read as the set of all finite subsets of A which contain z as a subset, for each finite subset z of A , form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsfbas.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
tsmsfbas.f ⊢ 𝐹 = ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
tsmsfbas.l ⊢ 𝐿 = ran 𝐹
tsmsfbas.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
Assertion tsmsfbas ( 𝜑 → 𝐿 ∈ ( fBas ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 tsmsfbas.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
2 tsmsfbas.f ⊢ 𝐹 = ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
3 tsmsfbas.l ⊢ 𝐿 = ran 𝐹
4 tsmsfbas.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
5 elex ⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V )
6 ssrab2 ⊢ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆
7 pwexg ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
8 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
9 7 8 syl ⊢ ( 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
10 1 9 eqeltrid ⊢ ( 𝐴 ∈ V → 𝑆 ∈ V )
11 10 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → 𝑆 ∈ V )
12 elpw2g ⊢ ( 𝑆 ∈ V → ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆 ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆 ) )
14 6 13 mpbiri ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ 𝒫 𝑆 )
15 14 2 fmptd ⊢ ( 𝐴 ∈ V → 𝐹 : 𝑆 ⟶ 𝒫 𝑆 )
16 15 frnd ⊢ ( 𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆 )
17 0ss ⊢ ∅ ⊆ 𝐴
18 0fin ⊢ ∅ ∈ Fin
19 elfpw ⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ∈ Fin ) )
20 17 18 19 mpbir2an ⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
21 20 1 eleqtrri ⊢ ∅ ∈ 𝑆
22 0ss ⊢ ∅ ⊆ 𝑦
23 22 rgenw ⊢ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦
24 rabid2 ⊢ ( 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 )
25 sseq1 ⊢ ( 𝑧 = ∅ → ( 𝑧 ⊆ 𝑦 ↔ ∅ ⊆ 𝑦 ) )
26 25 ralbidv ⊢ ( 𝑧 = ∅ → ( ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) )
27 24 26 syl5bb ⊢ ( 𝑧 = ∅ → ( 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) )
28 27 rspcev ⊢ ( ( ∅ ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ∅ ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
29 21 23 28 mp2an ⊢ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 }
30 2 elrnmpt ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
31 10 30 syl ⊢ ( 𝐴 ∈ V → ( 𝑆 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 𝑆 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
32 29 31 mpbiri ⊢ ( 𝐴 ∈ V → 𝑆 ∈ ran 𝐹 )
33 32 ne0d ⊢ ( 𝐴 ∈ V → ran 𝐹 ≠ ∅ )
34 simpr ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
35 ssid ⊢ 𝑧 ⊆ 𝑧
36 sseq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑧 ) )
37 36 rspcev ⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑧 ⊆ 𝑧 ) → ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 )
38 34 35 37 sylancl ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 )
39 rabn0 ⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 )
40 38 39 sylibr ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ≠ ∅ )
41 40 necomd ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ∅ ≠ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
42 41 neneqd ⊢ ( ( 𝐴 ∈ V ∧ 𝑧 ∈ 𝑆 ) → ¬ ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
43 42 nrexdv ⊢ ( 𝐴 ∈ V → ¬ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
44 0ex ⊢ ∅ ∈ V
45 2 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
46 44 45 ax-mp ⊢ ( ∅ ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑆 ∅ = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
47 43 46 sylnibr ⊢ ( 𝐴 ∈ V → ¬ ∅ ∈ ran 𝐹 )
48 df-nel ⊢ ( ∅ ∉ ran 𝐹 ↔ ¬ ∅ ∈ ran 𝐹 )
49 47 48 sylibr ⊢ ( 𝐴 ∈ V → ∅ ∉ ran 𝐹 )
50 elfpw ⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑢 ⊆ 𝐴 ∧ 𝑢 ∈ Fin ) )
51 50 simplbi ⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ⊆ 𝐴 )
52 51 1 eleq2s ⊢ ( 𝑢 ∈ 𝑆 → 𝑢 ⊆ 𝐴 )
53 elfpw ⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ∈ Fin ) )
54 53 simplbi ⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ⊆ 𝐴 )
55 54 1 eleq2s ⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ⊆ 𝐴 )
56 52 55 anim12i ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) )
57 unss ⊢ ( ( 𝑢 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴 ) ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 )
58 56 57 sylib ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 )
59 elinel2 ⊢ ( 𝑢 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑢 ∈ Fin )
60 59 1 eleq2s ⊢ ( 𝑢 ∈ 𝑆 → 𝑢 ∈ Fin )
61 elinel2 ⊢ ( 𝑣 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑣 ∈ Fin )
62 61 1 eleq2s ⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ∈ Fin )
63 unfi ⊢ ( ( 𝑢 ∈ Fin ∧ 𝑣 ∈ Fin ) → ( 𝑢 ∪ 𝑣 ) ∈ Fin )
64 60 62 63 syl2an ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ∈ Fin )
65 elfpw ⊢ ( ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑢 ∪ 𝑣 ) ⊆ 𝐴 ∧ ( 𝑢 ∪ 𝑣 ) ∈ Fin ) )
66 58 64 65 sylanbrc ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
67 66 adantl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 ∪ 𝑣 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
68 67 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 )
69 eqidd ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
70 sseq1 ⊢ ( 𝑎 = ( 𝑢 ∪ 𝑣 ) → ( 𝑎 ⊆ 𝑦 ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 ) )
71 70 rabbidv ⊢ ( 𝑎 = ( 𝑢 ∪ 𝑣 ) → { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
72 71 rspceeqv ⊢ ( ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) → ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } )
73 68 69 72 syl2anc ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } )
74 10 adantr ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝑆 ∈ V )
75 rabexg ⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V )
76 74 75 syl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V )
77 sseq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 ⊆ 𝑦 ↔ 𝑎 ⊆ 𝑦 ) )
78 77 rabbidv ⊢ ( 𝑧 = 𝑎 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } )
79 78 cbvmptv ⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑎 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } )
80 2 79 eqtri ⊢ 𝐹 = ( 𝑎 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } )
81 80 elrnmpt ⊢ ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V → ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) )
82 76 81 syl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑎 ⊆ 𝑦 } ) )
83 73 82 mpbird ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 )
84 pwidg ⊢ ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ V → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
85 76 84 syl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
86 inelcm ⊢ ( ( { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ ran 𝐹 ∧ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ∈ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) → ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ )
87 83 85 86 syl2anc ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ )
88 87 ralrimivva ⊢ ( 𝐴 ∈ V → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ )
89 rabexg ⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V )
90 10 89 syl ⊢ ( 𝐴 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V )
91 90 ralrimivw ⊢ ( 𝐴 ∈ V → ∀ 𝑢 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V )
92 sseq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 ⊆ 𝑦 ↔ 𝑢 ⊆ 𝑦 ) )
93 92 rabbidv ⊢ ( 𝑧 = 𝑢 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } )
94 93 cbvmptv ⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑢 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } )
95 2 94 eqtri ⊢ 𝐹 = ( 𝑢 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } )
96 ineq1 ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) )
97 inrab ⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) }
98 unss ⊢ ( ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) ↔ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 )
99 98 rabbii ⊢ { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ⊆ 𝑦 ∧ 𝑣 ⊆ 𝑦 ) } = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 }
100 97 99 eqtri ⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 }
101 96 100 eqtrdi ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
102 101 pweqd ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) = 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } )
103 102 ineq2d ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) = ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) )
104 103 neeq1d ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) )
105 104 ralbidv ⊢ ( 𝑎 = { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } → ( ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) )
106 95 105 ralrnmptw ⊢ ( ∀ 𝑢 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑢 ⊆ 𝑦 } ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) )
107 91 106 syl ⊢ ( 𝐴 ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 { 𝑦 ∈ 𝑆 ∣ ( 𝑢 ∪ 𝑣 ) ⊆ 𝑦 } ) ≠ ∅ ) )
108 88 107 mpbird ⊢ ( 𝐴 ∈ V → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ )
109 rabexg ⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V )
110 10 109 syl ⊢ ( 𝐴 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V )
111 110 ralrimivw ⊢ ( 𝐴 ∈ V → ∀ 𝑣 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V )
112 sseq1 ⊢ ( 𝑧 = 𝑣 → ( 𝑧 ⊆ 𝑦 ↔ 𝑣 ⊆ 𝑦 ) )
113 112 rabbidv ⊢ ( 𝑧 = 𝑣 → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } )
114 113 cbvmptv ⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑣 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } )
115 2 114 eqtri ⊢ 𝐹 = ( 𝑣 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } )
116 ineq2 ⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( 𝑎 ∩ 𝑏 ) = ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) )
117 116 pweqd ⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → 𝒫 ( 𝑎 ∩ 𝑏 ) = 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) )
118 117 ineq2d ⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) = ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) )
119 118 neeq1d ⊢ ( 𝑏 = { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } → ( ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) )
120 115 119 ralrnmptw ⊢ ( ∀ 𝑣 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ∈ V → ( ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) )
121 111 120 syl ⊢ ( 𝐴 ∈ V → ( ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) )
122 121 ralbidv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ↔ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑣 ∈ 𝑆 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ { 𝑦 ∈ 𝑆 ∣ 𝑣 ⊆ 𝑦 } ) ) ≠ ∅ ) )
123 108 122 mpbird ⊢ ( 𝐴 ∈ V → ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ )
124 33 49 123 3jca ⊢ ( 𝐴 ∈ V → ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) )
125 isfbas ⊢ ( 𝑆 ∈ V → ( ran 𝐹 ∈ ( fBas ‘ 𝑆 ) ↔ ( ran 𝐹 ⊆ 𝒫 𝑆 ∧ ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) ) ) )
126 10 125 syl ⊢ ( 𝐴 ∈ V → ( ran 𝐹 ∈ ( fBas ‘ 𝑆 ) ↔ ( ran 𝐹 ⊆ 𝒫 𝑆 ∧ ( ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀ 𝑎 ∈ ran 𝐹 ∀ 𝑏 ∈ ran 𝐹 ( ran 𝐹 ∩ 𝒫 ( 𝑎 ∩ 𝑏 ) ) ≠ ∅ ) ) ) )
127 16 124 126 mpbir2and ⊢ ( 𝐴 ∈ V → ran 𝐹 ∈ ( fBas ‘ 𝑆 ) )
128 3 127 eqeltrid ⊢ ( 𝐴 ∈ V → 𝐿 ∈ ( fBas ‘ 𝑆 ) )
129 4 5 128 3syl ⊢ ( 𝜑 → 𝐿 ∈ ( fBas ‘ 𝑆 ) )