Metamath Proof Explorer

Theorem fmfnfmlem4

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 19-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b ⊢φ→B∈fBas⁡Y
fmfnfm.l ⊢φ→L∈Fil⁡X
fmfnfm.f ⊢φ→F:Y⟶X
fmfnfm.fm ⊢φ→XFilMapF⁡B⊆L
Assertion fmfnfmlem4 ⊢φ→t∈L↔t⊆X∧∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢φ→B∈fBas⁡Y
2 fmfnfm.l ⊢φ→L∈Fil⁡X
3 fmfnfm.f ⊢φ→F:Y⟶X
4 fmfnfm.fm ⊢φ→XFilMapF⁡B⊆L
5 filelss ⊢L∈Fil⁡X∧t∈L→t⊆X
6 5 ex ⊢L∈Fil⁡X→t∈L→t⊆X
7 2 6 syl ⊢φ→t∈L→t⊆X
8 mptexg ⊢L∈Fil⁡X→x∈L⟼F-1x∈V
9 rnexg ⊢x∈L⟼F-1x∈V→ran⁡x∈L⟼F-1x∈V
10 8 9 syl ⊢L∈Fil⁡X→ran⁡x∈L⟼F-1x∈V
11 2 10 syl ⊢φ→ran⁡x∈L⟼F-1x∈V
12 unexg ⊢B∈fBas⁡Y∧ran⁡x∈L⟼F-1x∈V→B∪ran⁡x∈L⟼F-1x∈V
13 1 11 12 syl2anc ⊢φ→B∪ran⁡x∈L⟼F-1x∈V
14 ssfii ⊢B∪ran⁡x∈L⟼F-1x∈V→B∪ran⁡x∈L⟼F-1x⊆fi⁡B∪ran⁡x∈L⟼F-1x
15 14 unssbd ⊢B∪ran⁡x∈L⟼F-1x∈V→ran⁡x∈L⟼F-1x⊆fi⁡B∪ran⁡x∈L⟼F-1x
16 13 15 syl ⊢φ→ran⁡x∈L⟼F-1x⊆fi⁡B∪ran⁡x∈L⟼F-1x
17 16 adantr ⊢φ∧t∈L→ran⁡x∈L⟼F-1x⊆fi⁡B∪ran⁡x∈L⟼F-1x
18 eqid ⊢F-1t=F-1t
19 imaeq2 ⊢x=t→F-1x=F-1t
20 19 rspceeqv ⊢t∈L∧F-1t=F-1t→∃x∈LF-1t=F-1x
21 18 20 mpan2 ⊢t∈L→∃x∈LF-1t=F-1x
22 21 adantl ⊢φ∧t∈L→∃x∈LF-1t=F-1x
23 elfvdm ⊢B∈fBas⁡Y→Y∈dom⁡fBas
24 1 23 syl ⊢φ→Y∈dom⁡fBas
25 cnvimass ⊢F-1t⊆dom⁡F
26 25 3 fssdm ⊢φ→F-1t⊆Y
27 24 26 ssexd ⊢φ→F-1t∈V
28 27 adantr ⊢φ∧t∈L→F-1t∈V
29 eqid ⊢x∈L⟼F-1x=x∈L⟼F-1x
30 29 elrnmpt ⊢F-1t∈V→F-1t∈ran⁡x∈L⟼F-1x↔∃x∈LF-1t=F-1x
31 28 30 syl ⊢φ∧t∈L→F-1t∈ran⁡x∈L⟼F-1x↔∃x∈LF-1t=F-1x
32 22 31 mpbird ⊢φ∧t∈L→F-1t∈ran⁡x∈L⟼F-1x
33 17 32 sseldd ⊢φ∧t∈L→F-1t∈fi⁡B∪ran⁡x∈L⟼F-1x
34 ffun ⊢F:Y⟶X→Fun⁡F
35 ssid ⊢F-1t⊆F-1t
36 funimass2 ⊢Fun⁡F∧F-1t⊆F-1t→FF-1t⊆t
37 34 35 36 sylancl ⊢F:Y⟶X→FF-1t⊆t
38 3 37 syl ⊢φ→FF-1t⊆t
39 38 adantr ⊢φ∧t∈L→FF-1t⊆t
40 imaeq2 ⊢s=F-1t→Fs=FF-1t
41 40 sseq1d ⊢s=F-1t→Fs⊆t↔FF-1t⊆t
42 41 rspcev ⊢F-1t∈fi⁡B∪ran⁡x∈L⟼F-1x∧FF-1t⊆t→∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t
43 33 39 42 syl2anc ⊢φ∧t∈L→∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t
44 43 ex ⊢φ→t∈L→∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t
45 7 44 jcad ⊢φ→t∈L→t⊆X∧∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t
46 elfiun ⊢B∈fBas⁡Y∧ran⁡x∈L⟼F-1x∈V→s∈fi⁡B∪ran⁡x∈L⟼F-1x↔s∈fi⁡B∨s∈fi⁡ran⁡x∈L⟼F-1x∨∃z∈fi⁡B∃w∈fi⁡ran⁡x∈L⟼F-1xs=z∩w
47 1 11 46 syl2anc ⊢φ→s∈fi⁡B∪ran⁡x∈L⟼F-1x↔s∈fi⁡B∨s∈fi⁡ran⁡x∈L⟼F-1x∨∃z∈fi⁡B∃w∈fi⁡ran⁡x∈L⟼F-1xs=z∩w
48 1 2 3 4 fmfnfmlem1 ⊢φ→s∈fi⁡B→Fs⊆t→t⊆X→t∈L
49 1 2 3 4 fmfnfmlem3 ⊢φ→fi⁡ran⁡x∈L⟼F-1x=ran⁡x∈L⟼F-1x
50 49 eleq2d ⊢φ→s∈fi⁡ran⁡x∈L⟼F-1x↔s∈ran⁡x∈L⟼F-1x
51 29 elrnmpt ⊢s∈V→s∈ran⁡x∈L⟼F-1x↔∃x∈Ls=F-1x
52 51 elv ⊢s∈ran⁡x∈L⟼F-1x↔∃x∈Ls=F-1x
53 1 2 3 4 fmfnfmlem2 ⊢φ→∃x∈Ls=F-1x→Fs⊆t→t⊆X→t∈L
54 52 53 biimtrid ⊢φ→s∈ran⁡x∈L⟼F-1x→Fs⊆t→t⊆X→t∈L
55 50 54 sylbid ⊢φ→s∈fi⁡ran⁡x∈L⟼F-1x→Fs⊆t→t⊆X→t∈L
56 49 eleq2d ⊢φ→w∈fi⁡ran⁡x∈L⟼F-1x↔w∈ran⁡x∈L⟼F-1x
57 29 elrnmpt ⊢w∈V→w∈ran⁡x∈L⟼F-1x↔∃x∈Lw=F-1x
58 57 elv ⊢w∈ran⁡x∈L⟼F-1x↔∃x∈Lw=F-1x
59 56 58 bitrdi ⊢φ→w∈fi⁡ran⁡x∈L⟼F-1x↔∃x∈Lw=F-1x
60 59 adantr ⊢φ∧z∈fi⁡B→w∈fi⁡ran⁡x∈L⟼F-1x↔∃x∈Lw=F-1x
61 fbssfi ⊢B∈fBas⁡Y∧z∈fi⁡B→∃s∈Bs⊆z
62 1 61 sylan ⊢φ∧z∈fi⁡B→∃s∈Bs⊆z
63 2 ad3antrrr ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→L∈Fil⁡X
64 2 adantr ⊢φ∧s∈B∧s⊆z→L∈Fil⁡X
65 4 adantr ⊢φ∧s∈B→XFilMapF⁡B⊆L
66 filtop ⊢L∈Fil⁡X→X∈L
67 2 66 syl ⊢φ→X∈L
68 67 1 3 3jca ⊢φ→X∈L∧B∈fBas⁡Y∧F:Y⟶X
69 68 adantr ⊢φ∧s∈B→X∈L∧B∈fBas⁡Y∧F:Y⟶X
70 ssfg ⊢B∈fBas⁡Y→B⊆YfilGenB
71 1 70 syl ⊢φ→B⊆YfilGenB
72 71 sselda ⊢φ∧s∈B→s∈YfilGenB
73 eqid ⊢YfilGenB=YfilGenB
74 73 imaelfm ⊢X∈L∧B∈fBas⁡Y∧F:Y⟶X∧s∈YfilGenB→Fs∈XFilMapF⁡B
75 69 72 74 syl2anc ⊢φ∧s∈B→Fs∈XFilMapF⁡B
76 65 75 sseldd ⊢φ∧s∈B→Fs∈L
77 76 adantrr ⊢φ∧s∈B∧s⊆z→Fs∈L
78 64 77 jca ⊢φ∧s∈B∧s⊆z→L∈Fil⁡X∧Fs∈L
79 filin ⊢L∈Fil⁡X∧Fs∈L∧x∈L→Fs∩x∈L
80 79 3expa ⊢L∈Fil⁡X∧Fs∈L∧x∈L→Fs∩x∈L
81 78 80 sylan ⊢φ∧s∈B∧s⊆z∧x∈L→Fs∩x∈L
82 81 adantr ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→Fs∩x∈L
83 simprr ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→t⊆X
84 elin ⊢w∈Fs∩x↔w∈Fs∧w∈x
85 3 34 syl ⊢φ→Fun⁡F
86 fvelima ⊢Fun⁡F∧w∈Fs→∃y∈sF⁡y=w
87 86 ex ⊢Fun⁡F→w∈Fs→∃y∈sF⁡y=w
88 85 87 syl ⊢φ→w∈Fs→∃y∈sF⁡y=w
89 88 ad3antrrr ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X→w∈Fs→∃y∈sF⁡y=w
90 85 ad3antrrr ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→Fun⁡F
91 simplrr ⊢φ∧s∈B∧s⊆z∧x∈L→s⊆z
92 simprl ⊢t⊆X∧y∈s∧F⁡y∈x→y∈s
93 ssel2 ⊢s⊆z∧y∈s→y∈z
94 91 92 93 syl2an ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→y∈z
95 85 ad2antrr ⊢φ∧s∈B∧s⊆z∧y∈s→Fun⁡F
96 fbelss ⊢B∈fBas⁡Y∧s∈B→s⊆Y
97 1 96 sylan ⊢φ∧s∈B→s⊆Y
98 3 fdmd ⊢φ→dom⁡F=Y
99 98 adantr ⊢φ∧s∈B→dom⁡F=Y
100 97 99 sseqtrrd ⊢φ∧s∈B→s⊆dom⁡F
101 100 adantrr ⊢φ∧s∈B∧s⊆z→s⊆dom⁡F
102 101 sselda ⊢φ∧s∈B∧s⊆z∧y∈s→y∈dom⁡F
103 fvimacnv ⊢Fun⁡F∧y∈dom⁡F→F⁡y∈x↔y∈F-1x
104 95 102 103 syl2anc ⊢φ∧s∈B∧s⊆z∧y∈s→F⁡y∈x↔y∈F-1x
105 104 biimpd ⊢φ∧s∈B∧s⊆z∧y∈s→F⁡y∈x→y∈F-1x
106 105 impr ⊢φ∧s∈B∧s⊆z∧y∈s∧F⁡y∈x→y∈F-1x
107 106 ad2ant2rl ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→y∈F-1x
108 94 107 elind ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→y∈z∩F-1x
109 inss2 ⊢z∩F-1x⊆F-1x
110 cnvimass ⊢F-1x⊆dom⁡F
111 109 110 sstri ⊢z∩F-1x⊆dom⁡F
112 funfvima2 ⊢Fun⁡F∧z∩F-1x⊆dom⁡F→y∈z∩F-1x→F⁡y∈Fz∩F-1x
113 111 112 mpan2 ⊢Fun⁡F→y∈z∩F-1x→F⁡y∈Fz∩F-1x
114 90 108 113 sylc ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→F⁡y∈Fz∩F-1x
115 114 anassrs ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s∧F⁡y∈x→F⁡y∈Fz∩F-1x
116 115 expr ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s→F⁡y∈x→F⁡y∈Fz∩F-1x
117 eleq1 ⊢F⁡y=w→F⁡y∈x↔w∈x
118 eleq1 ⊢F⁡y=w→F⁡y∈Fz∩F-1x↔w∈Fz∩F-1x
119 117 118 imbi12d ⊢F⁡y=w→F⁡y∈x→F⁡y∈Fz∩F-1x↔w∈x→w∈Fz∩F-1x
120 116 119 syl5ibcom ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X∧y∈s→F⁡y=w→w∈x→w∈Fz∩F-1x
121 120 rexlimdva ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X→∃y∈sF⁡y=w→w∈x→w∈Fz∩F-1x
122 89 121 syld ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X→w∈Fs→w∈x→w∈Fz∩F-1x
123 122 impd ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X→w∈Fs∧w∈x→w∈Fz∩F-1x
124 84 123 biimtrid ⊢φ∧s∈B∧s⊆z∧x∈L∧t⊆X→w∈Fs∩x→w∈Fz∩F-1x
125 124 adantrl ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→w∈Fs∩x→w∈Fz∩F-1x
126 125 ssrdv ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→Fs∩x⊆Fz∩F-1x
127 simprl ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→Fz∩F-1x⊆t
128 126 127 sstrd ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→Fs∩x⊆t
129 filss ⊢L∈Fil⁡X∧Fs∩x∈L∧t⊆X∧Fs∩x⊆t→t∈L
130 63 82 83 128 129 syl13anc ⊢φ∧s∈B∧s⊆z∧x∈L∧Fz∩F-1x⊆t∧t⊆X→t∈L
131 130 exp32 ⊢φ∧s∈B∧s⊆z∧x∈L→Fz∩F-1x⊆t→t⊆X→t∈L
132 ineq2 ⊢w=F-1x→z∩w=z∩F-1x
133 132 imaeq2d ⊢w=F-1x→Fz∩w=Fz∩F-1x
134 133 sseq1d ⊢w=F-1x→Fz∩w⊆t↔Fz∩F-1x⊆t
135 134 imbi1d ⊢w=F-1x→Fz∩w⊆t→t⊆X→t∈L↔Fz∩F-1x⊆t→t⊆X→t∈L
136 131 135 syl5ibrcom ⊢φ∧s∈B∧s⊆z∧x∈L→w=F-1x→Fz∩w⊆t→t⊆X→t∈L
137 136 rexlimdva ⊢φ∧s∈B∧s⊆z→∃x∈Lw=F-1x→Fz∩w⊆t→t⊆X→t∈L
138 137 rexlimdvaa ⊢φ→∃s∈Bs⊆z→∃x∈Lw=F-1x→Fz∩w⊆t→t⊆X→t∈L
139 138 imp ⊢φ∧∃s∈Bs⊆z→∃x∈Lw=F-1x→Fz∩w⊆t→t⊆X→t∈L
140 62 139 syldan ⊢φ∧z∈fi⁡B→∃x∈Lw=F-1x→Fz∩w⊆t→t⊆X→t∈L
141 60 140 sylbid ⊢φ∧z∈fi⁡B→w∈fi⁡ran⁡x∈L⟼F-1x→Fz∩w⊆t→t⊆X→t∈L
142 141 impr ⊢φ∧z∈fi⁡B∧w∈fi⁡ran⁡x∈L⟼F-1x→Fz∩w⊆t→t⊆X→t∈L
143 imaeq2 ⊢s=z∩w→Fs=Fz∩w
144 143 sseq1d ⊢s=z∩w→Fs⊆t↔Fz∩w⊆t
145 144 imbi1d ⊢s=z∩w→Fs⊆t→t⊆X→t∈L↔Fz∩w⊆t→t⊆X→t∈L
146 142 145 syl5ibrcom ⊢φ∧z∈fi⁡B∧w∈fi⁡ran⁡x∈L⟼F-1x→s=z∩w→Fs⊆t→t⊆X→t∈L
147 146 rexlimdvva ⊢φ→∃z∈fi⁡B∃w∈fi⁡ran⁡x∈L⟼F-1xs=z∩w→Fs⊆t→t⊆X→t∈L
148 48 55 147 3jaod ⊢φ→s∈fi⁡B∨s∈fi⁡ran⁡x∈L⟼F-1x∨∃z∈fi⁡B∃w∈fi⁡ran⁡x∈L⟼F-1xs=z∩w→Fs⊆t→t⊆X→t∈L
149 47 148 sylbid ⊢φ→s∈fi⁡B∪ran⁡x∈L⟼F-1x→Fs⊆t→t⊆X→t∈L
150 149 rexlimdv ⊢φ→∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t→t⊆X→t∈L
151 150 impcomd ⊢φ→t⊆X∧∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t→t∈L
152 45 151 impbid ⊢φ→t∈L↔t⊆X∧∃s∈fi⁡B∪ran⁡x∈L⟼F-1xFs⊆t