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

Theorem tsmsfbas 21978
 Description: The collection of all sets of the form 𝐹(𝑧) = {𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦}, which can be read as the set of all finite subsets of 𝐴 which contain 𝑧 as a subset, for each finite subset 𝑧 of 𝐴, form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
tsmsfbas.s 𝑆 = (𝒫 𝐴 ∩ Fin)
tsmsfbas.f 𝐹 = (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦})
tsmsfbas.l 𝐿 = ran 𝐹
tsmsfbas.a (𝜑𝐴𝑊)
Assertion
Ref Expression
tsmsfbas (𝜑𝐿 ∈ (fBas‘𝑆))
Distinct variable groups:   𝑧,𝐴   𝑦,𝑧,𝑆
Allowed substitution hints:   𝜑(𝑦,𝑧)   𝐴(𝑦)   𝐹(𝑦,𝑧)   𝐿(𝑦,𝑧)   𝑊(𝑦,𝑧)

Proof of Theorem tsmsfbas
Dummy variables 𝑢 𝑎 𝑣 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsfbas.a . 2 (𝜑𝐴𝑊)
2 elex 3243 . 2 (𝐴𝑊𝐴 ∈ V)
3 tsmsfbas.l . . 3 𝐿 = ran 𝐹
4 ssrab2 3720 . . . . . . 7 {𝑦𝑆𝑧𝑦} ⊆ 𝑆
5 tsmsfbas.s . . . . . . . . . 10 𝑆 = (𝒫 𝐴 ∩ Fin)
6 pwexg 4880 . . . . . . . . . . 11 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
7 inex1g 4834 . . . . . . . . . . 11 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∩ Fin) ∈ V)
86, 7syl 17 . . . . . . . . . 10 (𝐴 ∈ V → (𝒫 𝐴 ∩ Fin) ∈ V)
95, 8syl5eqel 2734 . . . . . . . . 9 (𝐴 ∈ V → 𝑆 ∈ V)
109adantr 480 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝑧𝑆) → 𝑆 ∈ V)
11 elpw2g 4857 . . . . . . . 8 (𝑆 ∈ V → ({𝑦𝑆𝑧𝑦} ∈ 𝒫 𝑆 ↔ {𝑦𝑆𝑧𝑦} ⊆ 𝑆))
1210, 11syl 17 . . . . . . 7 ((𝐴 ∈ V ∧ 𝑧𝑆) → ({𝑦𝑆𝑧𝑦} ∈ 𝒫 𝑆 ↔ {𝑦𝑆𝑧𝑦} ⊆ 𝑆))
134, 12mpbiri 248 . . . . . 6 ((𝐴 ∈ V ∧ 𝑧𝑆) → {𝑦𝑆𝑧𝑦} ∈ 𝒫 𝑆)
14 tsmsfbas.f . . . . . 6 𝐹 = (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦})
1513, 14fmptd 6425 . . . . 5 (𝐴 ∈ V → 𝐹:𝑆⟶𝒫 𝑆)
16 frn 6091 . . . . 5 (𝐹:𝑆⟶𝒫 𝑆 → ran 𝐹 ⊆ 𝒫 𝑆)
1715, 16syl 17 . . . 4 (𝐴 ∈ V → ran 𝐹 ⊆ 𝒫 𝑆)
18 0ss 4005 . . . . . . . . . 10 ∅ ⊆ 𝐴
19 0fin 8229 . . . . . . . . . 10 ∅ ∈ Fin
20 elfpw 8309 . . . . . . . . . 10 (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
2118, 19, 20mpbir2an 975 . . . . . . . . 9 ∅ ∈ (𝒫 𝐴 ∩ Fin)
2221, 5eleqtrri 2729 . . . . . . . 8 ∅ ∈ 𝑆
23 0ss 4005 . . . . . . . . 9 ∅ ⊆ 𝑦
2423rgenw 2953 . . . . . . . 8 𝑦𝑆 ∅ ⊆ 𝑦
25 rabid2 3148 . . . . . . . . . 10 (𝑆 = {𝑦𝑆𝑧𝑦} ↔ ∀𝑦𝑆 𝑧𝑦)
26 sseq1 3659 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑧𝑦 ↔ ∅ ⊆ 𝑦))
2726ralbidv 3015 . . . . . . . . . 10 (𝑧 = ∅ → (∀𝑦𝑆 𝑧𝑦 ↔ ∀𝑦𝑆 ∅ ⊆ 𝑦))
2825, 27syl5bb 272 . . . . . . . . 9 (𝑧 = ∅ → (𝑆 = {𝑦𝑆𝑧𝑦} ↔ ∀𝑦𝑆 ∅ ⊆ 𝑦))
2928rspcev 3340 . . . . . . . 8 ((∅ ∈ 𝑆 ∧ ∀𝑦𝑆 ∅ ⊆ 𝑦) → ∃𝑧𝑆 𝑆 = {𝑦𝑆𝑧𝑦})
3022, 24, 29mp2an 708 . . . . . . 7 𝑧𝑆 𝑆 = {𝑦𝑆𝑧𝑦}
3114elrnmpt 5404 . . . . . . . 8 (𝑆 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧𝑆 𝑆 = {𝑦𝑆𝑧𝑦}))
329, 31syl 17 . . . . . . 7 (𝐴 ∈ V → (𝑆 ∈ ran 𝐹 ↔ ∃𝑧𝑆 𝑆 = {𝑦𝑆𝑧𝑦}))
3330, 32mpbiri 248 . . . . . 6 (𝐴 ∈ V → 𝑆 ∈ ran 𝐹)
34 ne0i 3954 . . . . . 6 (𝑆 ∈ ran 𝐹 → ran 𝐹 ≠ ∅)
3533, 34syl 17 . . . . 5 (𝐴 ∈ V → ran 𝐹 ≠ ∅)
36 simpr 476 . . . . . . . . . . . 12 ((𝐴 ∈ V ∧ 𝑧𝑆) → 𝑧𝑆)
37 ssid 3657 . . . . . . . . . . . 12 𝑧𝑧
38 sseq2 3660 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑧𝑦𝑧𝑧))
3938rspcev 3340 . . . . . . . . . . . 12 ((𝑧𝑆𝑧𝑧) → ∃𝑦𝑆 𝑧𝑦)
4036, 37, 39sylancl 695 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ 𝑧𝑆) → ∃𝑦𝑆 𝑧𝑦)
41 rabn0 3991 . . . . . . . . . . 11 ({𝑦𝑆𝑧𝑦} ≠ ∅ ↔ ∃𝑦𝑆 𝑧𝑦)
4240, 41sylibr 224 . . . . . . . . . 10 ((𝐴 ∈ V ∧ 𝑧𝑆) → {𝑦𝑆𝑧𝑦} ≠ ∅)
4342necomd 2878 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝑧𝑆) → ∅ ≠ {𝑦𝑆𝑧𝑦})
4443neneqd 2828 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝑧𝑆) → ¬ ∅ = {𝑦𝑆𝑧𝑦})
4544nrexdv 3030 . . . . . . 7 (𝐴 ∈ V → ¬ ∃𝑧𝑆 ∅ = {𝑦𝑆𝑧𝑦})
46 0ex 4823 . . . . . . . 8 ∅ ∈ V
4714elrnmpt 5404 . . . . . . . 8 (∅ ∈ V → (∅ ∈ ran 𝐹 ↔ ∃𝑧𝑆 ∅ = {𝑦𝑆𝑧𝑦}))
4846, 47ax-mp 5 . . . . . . 7 (∅ ∈ ran 𝐹 ↔ ∃𝑧𝑆 ∅ = {𝑦𝑆𝑧𝑦})
4945, 48sylnibr 318 . . . . . 6 (𝐴 ∈ V → ¬ ∅ ∈ ran 𝐹)
50 df-nel 2927 . . . . . 6 (∅ ∉ ran 𝐹 ↔ ¬ ∅ ∈ ran 𝐹)
5149, 50sylibr 224 . . . . 5 (𝐴 ∈ V → ∅ ∉ ran 𝐹)
52 elfpw 8309 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑢𝐴𝑢 ∈ Fin))
5352simplbi 475 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢𝐴)
5453, 5eleq2s 2748 . . . . . . . . . . . . . . . 16 (𝑢𝑆𝑢𝐴)
55 elfpw 8309 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑣𝐴𝑣 ∈ Fin))
5655simplbi 475 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣𝐴)
5756, 5eleq2s 2748 . . . . . . . . . . . . . . . 16 (𝑣𝑆𝑣𝐴)
5854, 57anim12i 589 . . . . . . . . . . . . . . 15 ((𝑢𝑆𝑣𝑆) → (𝑢𝐴𝑣𝐴))
59 unss 3820 . . . . . . . . . . . . . . 15 ((𝑢𝐴𝑣𝐴) ↔ (𝑢𝑣) ⊆ 𝐴)
6058, 59sylib 208 . . . . . . . . . . . . . 14 ((𝑢𝑆𝑣𝑆) → (𝑢𝑣) ⊆ 𝐴)
6152simprbi 479 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (𝒫 𝐴 ∩ Fin) → 𝑢 ∈ Fin)
6261, 5eleq2s 2748 . . . . . . . . . . . . . . 15 (𝑢𝑆𝑢 ∈ Fin)
6355simprbi 479 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝒫 𝐴 ∩ Fin) → 𝑣 ∈ Fin)
6463, 5eleq2s 2748 . . . . . . . . . . . . . . 15 (𝑣𝑆𝑣 ∈ Fin)
65 unfi 8268 . . . . . . . . . . . . . . 15 ((𝑢 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑢𝑣) ∈ Fin)
6662, 64, 65syl2an 493 . . . . . . . . . . . . . 14 ((𝑢𝑆𝑣𝑆) → (𝑢𝑣) ∈ Fin)
67 elfpw 8309 . . . . . . . . . . . . . 14 ((𝑢𝑣) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑢𝑣) ⊆ 𝐴 ∧ (𝑢𝑣) ∈ Fin))
6860, 66, 67sylanbrc 699 . . . . . . . . . . . . 13 ((𝑢𝑆𝑣𝑆) → (𝑢𝑣) ∈ (𝒫 𝐴 ∩ Fin))
6968adantl 481 . . . . . . . . . . . 12 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝑣) ∈ (𝒫 𝐴 ∩ Fin))
7069, 5syl6eleqr 2741 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → (𝑢𝑣) ∈ 𝑆)
71 eqidd 2652 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
72 sseq1 3659 . . . . . . . . . . . . . 14 (𝑎 = (𝑢𝑣) → (𝑎𝑦 ↔ (𝑢𝑣) ⊆ 𝑦))
7372rabbidv 3220 . . . . . . . . . . . . 13 (𝑎 = (𝑢𝑣) → {𝑦𝑆𝑎𝑦} = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
7473eqeq2d 2661 . . . . . . . . . . . 12 (𝑎 = (𝑢𝑣) → ({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆𝑎𝑦} ↔ {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}))
7574rspcev 3340 . . . . . . . . . . 11 (((𝑢𝑣) ∈ 𝑆 ∧ {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) → ∃𝑎𝑆 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆𝑎𝑦})
7670, 71, 75syl2anc 694 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → ∃𝑎𝑆 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆𝑎𝑦})
779adantr 480 . . . . . . . . . . . 12 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → 𝑆 ∈ V)
78 rabexg 4844 . . . . . . . . . . . 12 (𝑆 ∈ V → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ V)
7977, 78syl 17 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ V)
80 sseq1 3659 . . . . . . . . . . . . . . 15 (𝑧 = 𝑎 → (𝑧𝑦𝑎𝑦))
8180rabbidv 3220 . . . . . . . . . . . . . 14 (𝑧 = 𝑎 → {𝑦𝑆𝑧𝑦} = {𝑦𝑆𝑎𝑦})
8281cbvmptv 4783 . . . . . . . . . . . . 13 (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}) = (𝑎𝑆 ↦ {𝑦𝑆𝑎𝑦})
8314, 82eqtri 2673 . . . . . . . . . . . 12 𝐹 = (𝑎𝑆 ↦ {𝑦𝑆𝑎𝑦})
8483elrnmpt 5404 . . . . . . . . . . 11 ({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ V → ({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎𝑆 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆𝑎𝑦}))
8579, 84syl 17 . . . . . . . . . 10 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → ({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ ran 𝐹 ↔ ∃𝑎𝑆 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} = {𝑦𝑆𝑎𝑦}))
8676, 85mpbird 247 . . . . . . . . 9 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ ran 𝐹)
87 pwidg 4206 . . . . . . . . . 10 ({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ V → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
8879, 87syl 17 . . . . . . . . 9 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
89 inelcm 4065 . . . . . . . . 9 (({𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ ran 𝐹 ∧ {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦} ∈ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) → (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅)
9086, 88, 89syl2anc 694 . . . . . . . 8 ((𝐴 ∈ V ∧ (𝑢𝑆𝑣𝑆)) → (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅)
9190ralrimivva 3000 . . . . . . 7 (𝐴 ∈ V → ∀𝑢𝑆𝑣𝑆 (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅)
92 rabexg 4844 . . . . . . . . . 10 (𝑆 ∈ V → {𝑦𝑆𝑢𝑦} ∈ V)
939, 92syl 17 . . . . . . . . 9 (𝐴 ∈ V → {𝑦𝑆𝑢𝑦} ∈ V)
9493ralrimivw 2996 . . . . . . . 8 (𝐴 ∈ V → ∀𝑢𝑆 {𝑦𝑆𝑢𝑦} ∈ V)
95 sseq1 3659 . . . . . . . . . . . 12 (𝑧 = 𝑢 → (𝑧𝑦𝑢𝑦))
9695rabbidv 3220 . . . . . . . . . . 11 (𝑧 = 𝑢 → {𝑦𝑆𝑧𝑦} = {𝑦𝑆𝑢𝑦})
9796cbvmptv 4783 . . . . . . . . . 10 (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}) = (𝑢𝑆 ↦ {𝑦𝑆𝑢𝑦})
9814, 97eqtri 2673 . . . . . . . . 9 𝐹 = (𝑢𝑆 ↦ {𝑦𝑆𝑢𝑦})
99 ineq1 3840 . . . . . . . . . . . . . 14 (𝑎 = {𝑦𝑆𝑢𝑦} → (𝑎 ∩ {𝑦𝑆𝑣𝑦}) = ({𝑦𝑆𝑢𝑦} ∩ {𝑦𝑆𝑣𝑦}))
100 inrab 3932 . . . . . . . . . . . . . . 15 ({𝑦𝑆𝑢𝑦} ∩ {𝑦𝑆𝑣𝑦}) = {𝑦𝑆 ∣ (𝑢𝑦𝑣𝑦)}
101 unss 3820 . . . . . . . . . . . . . . . 16 ((𝑢𝑦𝑣𝑦) ↔ (𝑢𝑣) ⊆ 𝑦)
102101rabbii 3216 . . . . . . . . . . . . . . 15 {𝑦𝑆 ∣ (𝑢𝑦𝑣𝑦)} = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}
103100, 102eqtri 2673 . . . . . . . . . . . . . 14 ({𝑦𝑆𝑢𝑦} ∩ {𝑦𝑆𝑣𝑦}) = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}
10499, 103syl6eq 2701 . . . . . . . . . . . . 13 (𝑎 = {𝑦𝑆𝑢𝑦} → (𝑎 ∩ {𝑦𝑆𝑣𝑦}) = {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
105104pweqd 4196 . . . . . . . . . . . 12 (𝑎 = {𝑦𝑆𝑢𝑦} → 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦}) = 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦})
106105ineq2d 3847 . . . . . . . . . . 11 (𝑎 = {𝑦𝑆𝑢𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) = (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}))
107106neeq1d 2882 . . . . . . . . . 10 (𝑎 = {𝑦𝑆𝑢𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅))
108107ralbidv 3015 . . . . . . . . 9 (𝑎 = {𝑦𝑆𝑢𝑦} → (∀𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅ ↔ ∀𝑣𝑆 (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅))
10998, 108ralrnmpt 6408 . . . . . . . 8 (∀𝑢𝑆 {𝑦𝑆𝑢𝑦} ∈ V → (∀𝑎 ∈ ran 𝐹𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅ ↔ ∀𝑢𝑆𝑣𝑆 (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅))
11094, 109syl 17 . . . . . . 7 (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅ ↔ ∀𝑢𝑆𝑣𝑆 (ran 𝐹 ∩ 𝒫 {𝑦𝑆 ∣ (𝑢𝑣) ⊆ 𝑦}) ≠ ∅))
11191, 110mpbird 247 . . . . . 6 (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅)
112 rabexg 4844 . . . . . . . . . 10 (𝑆 ∈ V → {𝑦𝑆𝑣𝑦} ∈ V)
1139, 112syl 17 . . . . . . . . 9 (𝐴 ∈ V → {𝑦𝑆𝑣𝑦} ∈ V)
114113ralrimivw 2996 . . . . . . . 8 (𝐴 ∈ V → ∀𝑣𝑆 {𝑦𝑆𝑣𝑦} ∈ V)
115 sseq1 3659 . . . . . . . . . . . 12 (𝑧 = 𝑣 → (𝑧𝑦𝑣𝑦))
116115rabbidv 3220 . . . . . . . . . . 11 (𝑧 = 𝑣 → {𝑦𝑆𝑧𝑦} = {𝑦𝑆𝑣𝑦})
117116cbvmptv 4783 . . . . . . . . . 10 (𝑧𝑆 ↦ {𝑦𝑆𝑧𝑦}) = (𝑣𝑆 ↦ {𝑦𝑆𝑣𝑦})
11814, 117eqtri 2673 . . . . . . . . 9 𝐹 = (𝑣𝑆 ↦ {𝑦𝑆𝑣𝑦})
119 ineq2 3841 . . . . . . . . . . . 12 (𝑏 = {𝑦𝑆𝑣𝑦} → (𝑎𝑏) = (𝑎 ∩ {𝑦𝑆𝑣𝑦}))
120119pweqd 4196 . . . . . . . . . . 11 (𝑏 = {𝑦𝑆𝑣𝑦} → 𝒫 (𝑎𝑏) = 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦}))
121120ineq2d 3847 . . . . . . . . . 10 (𝑏 = {𝑦𝑆𝑣𝑦} → (ran 𝐹 ∩ 𝒫 (𝑎𝑏)) = (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})))
122121neeq1d 2882 . . . . . . . . 9 (𝑏 = {𝑦𝑆𝑣𝑦} → ((ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅ ↔ (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅))
123118, 122ralrnmpt 6408 . . . . . . . 8 (∀𝑣𝑆 {𝑦𝑆𝑣𝑦} ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅ ↔ ∀𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅))
124114, 123syl 17 . . . . . . 7 (𝐴 ∈ V → (∀𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅ ↔ ∀𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅))
125124ralbidv 3015 . . . . . 6 (𝐴 ∈ V → (∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅ ↔ ∀𝑎 ∈ ran 𝐹𝑣𝑆 (ran 𝐹 ∩ 𝒫 (𝑎 ∩ {𝑦𝑆𝑣𝑦})) ≠ ∅))
126111, 125mpbird 247 . . . . 5 (𝐴 ∈ V → ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅)
12735, 51, 1263jca 1261 . . . 4 (𝐴 ∈ V → (ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅))
128 isfbas 21680 . . . . 5 (𝑆 ∈ V → (ran 𝐹 ∈ (fBas‘𝑆) ↔ (ran 𝐹 ⊆ 𝒫 𝑆 ∧ (ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅))))
1299, 128syl 17 . . . 4 (𝐴 ∈ V → (ran 𝐹 ∈ (fBas‘𝑆) ↔ (ran 𝐹 ⊆ 𝒫 𝑆 ∧ (ran 𝐹 ≠ ∅ ∧ ∅ ∉ ran 𝐹 ∧ ∀𝑎 ∈ ran 𝐹𝑏 ∈ ran 𝐹(ran 𝐹 ∩ 𝒫 (𝑎𝑏)) ≠ ∅))))
13017, 127, 129mpbir2and 977 . . 3 (𝐴 ∈ V → ran 𝐹 ∈ (fBas‘𝑆))
1313, 130syl5eqel 2734 . 2 (𝐴 ∈ V → 𝐿 ∈ (fBas‘𝑆))
1321, 2, 1313syl 18 1 (𝜑𝐿 ∈ (fBas‘𝑆))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823   ∉ wnel 2926  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191   ↦ cmpt 4762  ran crn 5144  ⟶wf 5922  ‘cfv 5926  Fincfn 7997  fBascfbas 19782 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-er 7787  df-en 7998  df-fin 8001  df-fbas 19791 This theorem is referenced by:  eltsms  21983  haustsms  21986  tsmscls  21988  tsmsmhm  21996  tsmsadd  21997
 Copyright terms: Public domain W3C validator