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 ‘ 𝑆 ) )