Metamath Proof Explorer

Theorem fbasrn

Description: Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbasrn.c ⊢ 𝐶 = ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) )
Assertion fbasrn ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐶 ∈ ( fBas ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 fbasrn.c ⊢ 𝐶 = ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) )
2 simpl3 ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑌 ∈ 𝑉 )
3 simpl2 ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
4 fimass ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝐹 “ 𝑥 ) ⊆ 𝑌 )
5 3 4 syl ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑌 )
6 2 5 sselpwd ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ∈ 𝒫 𝑌 )
7 6 fmpttd ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐵 ⟶ 𝒫 𝑌 )
8 7 frnd ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ⊆ 𝒫 𝑌 )
9 1 8 eqsstrid ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐶 ⊆ 𝒫 𝑌 )
10 1 a1i ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐶 = ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) )
11 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
12 11 3ad2ant2 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → Fun 𝐹 )
13 funimaexg ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 “ 𝑥 ) ∈ V )
14 13 ralrimiva ⊢ ( Fun 𝐹 → ∀ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ∈ V )
15 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑥 ) ∈ V → dom ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = 𝐵 )
16 12 14 15 3syl ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = 𝐵 )
17 fbasne0 ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐵 ≠ ∅ )
18 17 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐵 ≠ ∅ )
19 16 18 eqnetrd ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ≠ ∅ )
20 dm0rn0 ⊢ ( dom ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = ∅ ↔ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = ∅ )
21 20 necon3bii ⊢ ( dom ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ≠ ∅ ↔ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ≠ ∅ )
22 19 21 sylib ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ≠ ∅ )
23 10 22 eqnetrd ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐶 ≠ ∅ )
24 fbelss ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ⊆ 𝑋 )
25 24 ex ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋 ) )
26 25 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ 𝑋 ) )
27 0nelfb ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐵 )
28 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐵 ↔ ∅ ∈ 𝐵 ) )
29 28 notbid ⊢ ( 𝑥 = ∅ → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ ∅ ∈ 𝐵 ) )
30 27 29 syl5ibrcom ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 = ∅ → ¬ 𝑥 ∈ 𝐵 ) )
31 30 con2d ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅ ) )
32 31 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 → ¬ 𝑥 = ∅ ) )
33 26 32 jcad ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅ ) ) )
34 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
35 34 3ad2ant2 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → dom 𝐹 = 𝑋 )
36 35 sseq2d ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ⊆ dom 𝐹 ↔ 𝑥 ⊆ 𝑋 ) )
37 36 biimpar ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ⊆ dom 𝐹 )
38 sseqin2 ⊢ ( 𝑥 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑥 ) = 𝑥 )
39 37 38 sylib ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ⊆ 𝑋 ) → ( dom 𝐹 ∩ 𝑥 ) = 𝑥 )
40 39 eqeq1d ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( dom 𝐹 ∩ 𝑥 ) = ∅ ↔ 𝑥 = ∅ ) )
41 40 biimpd ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( dom 𝐹 ∩ 𝑥 ) = ∅ → 𝑥 = ∅ ) )
42 41 con3d ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 = ∅ → ¬ ( dom 𝐹 ∩ 𝑥 ) = ∅ ) )
43 42 expimpd ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅ ) → ¬ ( dom 𝐹 ∩ 𝑥 ) = ∅ ) )
44 eqcom ⊢ ( ∅ = ( 𝐹 “ 𝑥 ) ↔ ( 𝐹 “ 𝑥 ) = ∅ )
45 imadisj ⊢ ( ( 𝐹 “ 𝑥 ) = ∅ ↔ ( dom 𝐹 ∩ 𝑥 ) = ∅ )
46 44 45 bitri ⊢ ( ∅ = ( 𝐹 “ 𝑥 ) ↔ ( dom 𝐹 ∩ 𝑥 ) = ∅ )
47 46 notbii ⊢ ( ¬ ∅ = ( 𝐹 “ 𝑥 ) ↔ ¬ ( dom 𝐹 ∩ 𝑥 ) = ∅ )
48 43 47 imbitrrdi ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 = ∅ ) → ¬ ∅ = ( 𝐹 “ 𝑥 ) ) )
49 33 48 syld ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐵 → ¬ ∅ = ( 𝐹 “ 𝑥 ) ) )
50 49 ralrimiv ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐵 ¬ ∅ = ( 𝐹 “ 𝑥 ) )
51 1 eleq2i ⊢ ( ∅ ∈ 𝐶 ↔ ∅ ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) )
52 0ex ⊢ ∅ ∈ V
53 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) )
54 53 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∅ = ( 𝐹 “ 𝑥 ) ) )
55 52 54 ax-mp ⊢ ( ∅ ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∅ = ( 𝐹 “ 𝑥 ) )
56 51 55 bitri ⊢ ( ∅ ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 ∅ = ( 𝐹 “ 𝑥 ) )
57 56 notbii ⊢ ( ¬ ∅ ∈ 𝐶 ↔ ¬ ∃ 𝑥 ∈ 𝐵 ∅ = ( 𝐹 “ 𝑥 ) )
58 df-nel ⊢ ( ∅ ∉ 𝐶 ↔ ¬ ∅ ∈ 𝐶 )
59 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐵 ¬ ∅ = ( 𝐹 “ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ 𝐵 ∅ = ( 𝐹 “ 𝑥 ) )
60 57 58 59 3bitr4i ⊢ ( ∅ ∉ 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 ¬ ∅ = ( 𝐹 “ 𝑥 ) )
61 50 60 sylibr ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ∅ ∉ 𝐶 )
62 1 eleq2i ⊢ ( 𝑟 ∈ 𝐶 ↔ 𝑟 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) )
63 imaeq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑢 ) )
64 63 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑢 ∈ 𝐵 ↦ ( 𝐹 “ 𝑢 ) )
65 64 elrnmpt ⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑢 ∈ 𝐵 𝑟 = ( 𝐹 “ 𝑢 ) ) )
66 65 elv ⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑢 ∈ 𝐵 𝑟 = ( 𝐹 “ 𝑢 ) )
67 62 66 bitri ⊢ ( 𝑟 ∈ 𝐶 ↔ ∃ 𝑢 ∈ 𝐵 𝑟 = ( 𝐹 “ 𝑢 ) )
68 1 eleq2i ⊢ ( 𝑠 ∈ 𝐶 ↔ 𝑠 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) )
69 imaeq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑣 ) )
70 69 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑣 ∈ 𝐵 ↦ ( 𝐹 “ 𝑣 ) )
71 70 elrnmpt ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑣 ∈ 𝐵 𝑠 = ( 𝐹 “ 𝑣 ) ) )
72 71 elv ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑣 ∈ 𝐵 𝑠 = ( 𝐹 “ 𝑣 ) )
73 68 72 bitri ⊢ ( 𝑠 ∈ 𝐶 ↔ ∃ 𝑣 ∈ 𝐵 𝑠 = ( 𝐹 “ 𝑣 ) )
74 67 73 anbi12i ⊢ ( ( 𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶 ) ↔ ( ∃ 𝑢 ∈ 𝐵 𝑟 = ( 𝐹 “ 𝑢 ) ∧ ∃ 𝑣 ∈ 𝐵 𝑠 = ( 𝐹 “ 𝑣 ) ) )
75 reeanv ⊢ ( ∃ 𝑢 ∈ 𝐵 ∃ 𝑣 ∈ 𝐵 ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ↔ ( ∃ 𝑢 ∈ 𝐵 𝑟 = ( 𝐹 “ 𝑢 ) ∧ ∃ 𝑣 ∈ 𝐵 𝑠 = ( 𝐹 “ 𝑣 ) ) )
76 74 75 bitr4i ⊢ ( ( 𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶 ) ↔ ∃ 𝑢 ∈ 𝐵 ∃ 𝑣 ∈ 𝐵 ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) )
77 fbasssin ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) )
78 77 3expb ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) )
79 78 3ad2antl1 ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) )
80 79 adantrr ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) )
81 eqid ⊢ ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑤 )
82 imaeq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑤 ) )
83 82 rspceeqv ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑤 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) )
84 81 83 mpan2 ⊢ ( 𝑤 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) )
85 84 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) )
86 1 eleq2i ⊢ ( ( 𝐹 “ 𝑤 ) ∈ 𝐶 ↔ ( 𝐹 “ 𝑤 ) ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) )
87 vex ⊢ 𝑤 ∈ V
88 87 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝑤 ) ∈ V )
89 53 elrnmpt ⊢ ( ( 𝐹 “ 𝑤 ) ∈ V → ( ( 𝐹 “ 𝑤 ) ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) ) )
90 12 88 89 3syl ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 “ 𝑤 ) ∈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) ) )
91 86 90 bitrid ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 “ 𝑤 ) ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) ) )
92 91 ad2antrr ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( ( 𝐹 “ 𝑤 ) ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑥 ) ) )
93 85 92 mpbird ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( 𝐹 “ 𝑤 ) ∈ 𝐶 )
94 imass2 ⊢ ( 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) )
95 94 ad2antll ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) )
96 inss1 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢
97 imass2 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 → ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝐹 “ 𝑢 ) )
98 96 97 ax-mp ⊢ ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝐹 “ 𝑢 )
99 inss2 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣
100 imass2 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣 → ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝐹 “ 𝑣 ) )
101 99 100 ax-mp ⊢ ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝐹 “ 𝑣 )
102 98 101 ssini ⊢ ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( ( 𝐹 “ 𝑢 ) ∩ ( 𝐹 “ 𝑣 ) )
103 ineq12 ⊢ ( ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) → ( 𝑟 ∩ 𝑠 ) = ( ( 𝐹 “ 𝑢 ) ∩ ( 𝐹 “ 𝑣 ) ) )
104 103 ad2antlr ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( 𝑟 ∩ 𝑠 ) = ( ( 𝐹 “ 𝑢 ) ∩ ( 𝐹 “ 𝑣 ) ) )
105 102 104 sseqtrrid ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( 𝐹 “ ( 𝑢 ∩ 𝑣 ) ) ⊆ ( 𝑟 ∩ 𝑠 ) )
106 95 105 sstrd ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝑟 ∩ 𝑠 ) )
107 sseq1 ⊢ ( 𝑧 = ( 𝐹 “ 𝑤 ) → ( 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ↔ ( 𝐹 “ 𝑤 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) )
108 107 rspcev ⊢ ( ( ( 𝐹 “ 𝑤 ) ∈ 𝐶 ∧ ( 𝐹 “ 𝑤 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) )
109 93 106 108 syl2anc ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) )
110 109 adantlrl ⊢ ( ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) )
111 80 110 rexlimddv ⊢ ( ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) ∧ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) )
112 111 exp32 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) )
113 112 rexlimdvv ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑢 ∈ 𝐵 ∃ 𝑣 ∈ 𝐵 ( 𝑟 = ( 𝐹 “ 𝑢 ) ∧ 𝑠 = ( 𝐹 “ 𝑣 ) ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
114 76 113 biimtrid ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑟 ∈ 𝐶 ∧ 𝑠 ∈ 𝐶 ) → ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
115 114 ralrimivv ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ∀ 𝑟 ∈ 𝐶 ∀ 𝑠 ∈ 𝐶 ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) )
116 23 61 115 3jca ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀ 𝑟 ∈ 𝐶 ∀ 𝑠 ∈ 𝐶 ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) )
117 isfbas2 ⊢ ( 𝑌 ∈ 𝑉 → ( 𝐶 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐶 ⊆ 𝒫 𝑌 ∧ ( 𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀ 𝑟 ∈ 𝐶 ∀ 𝑠 ∈ 𝐶 ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
118 117 3ad2ant3 ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐶 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐶 ⊆ 𝒫 𝑌 ∧ ( 𝐶 ≠ ∅ ∧ ∅ ∉ 𝐶 ∧ ∀ 𝑟 ∈ 𝐶 ∀ 𝑠 ∈ 𝐶 ∃ 𝑧 ∈ 𝐶 𝑧 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) )
119 9 116 118 mpbir2and ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐶 ∈ ( fBas ‘ 𝑌 ) )