Metamath Proof Explorer

Theorem fnemeet2

Description: The meet of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 6-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion fnemeet2 ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)↔\left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)$

Proof

Step Hyp Ref Expression
1 riin0 ${⊢}{S}=\varnothing \to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)=𝒫{X}$
2 1 unieqd ${⊢}{S}=\varnothing \to \bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)=\bigcup 𝒫{X}$
3 unipw ${⊢}\bigcup 𝒫{X}={X}$
4 2 3 syl6req ${⊢}{S}=\varnothing \to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
5 4 a1i ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({S}=\varnothing \to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
6 n0 ${⊢}{S}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
7 unieq ${⊢}{y}={x}\to \bigcup {y}=\bigcup {x}$
8 7 eqeq2d ${⊢}{y}={x}\to \left({X}=\bigcup {y}↔{X}=\bigcup {x}\right)$
9 8 rspccva ${⊢}\left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to {X}=\bigcup {x}$
10 9 3adant1 ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to {X}=\bigcup {x}$
11 fnemeet1 ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\mathrm{Fne}{x}$
12 eqid ${⊢}\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
13 eqid ${⊢}\bigcup {x}=\bigcup {x}$
14 12 13 fnebas ${⊢}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\mathrm{Fne}{x}\to \bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)=\bigcup {x}$
15 11 14 syl ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to \bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)=\bigcup {x}$
16 10 15 eqtr4d ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
17 16 3expia ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({x}\in {S}\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
18 17 exlimdv ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {S}\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
19 6 18 syl5bi ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({S}\ne \varnothing \to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
20 5 19 pm2.61dne ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
21 20 adantr ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge {T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
22 eqid ${⊢}\bigcup {T}=\bigcup {T}$
23 22 12 fnebas ${⊢}{T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to \bigcup {T}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
24 23 adantl ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge {T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)\to \bigcup {T}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
25 21 24 eqtr4d ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge {T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)\to {X}=\bigcup {T}$
26 25 ex ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to {X}=\bigcup {T}\right)$
27 fnetr ${⊢}\left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\wedge \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\mathrm{Fne}{x}\right)\to {T}\mathrm{Fne}{x}$
28 27 expcom ${⊢}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\mathrm{Fne}{x}\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to {T}\mathrm{Fne}{x}\right)$
29 11 28 syl ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\wedge {x}\in {S}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to {T}\mathrm{Fne}{x}\right)$
30 29 3expa ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge {x}\in {S}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to {T}\mathrm{Fne}{x}\right)$
31 30 ralrimdva ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)$
32 26 31 jcad ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\to \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)$
33 simprl ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {X}=\bigcup {T}$
34 20 adantr ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {X}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
35 33 34 eqtr3d ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to \bigcup {T}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
36 eqimss2 ${⊢}{X}=\bigcup {T}\to \bigcup {T}\subseteq {X}$
37 36 ad2antrl ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to \bigcup {T}\subseteq {X}$
38 sspwuni ${⊢}{T}\subseteq 𝒫{X}↔\bigcup {T}\subseteq {X}$
39 37 38 sylibr ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {T}\subseteq 𝒫{X}$
40 breq2 ${⊢}{x}={t}\to \left({T}\mathrm{Fne}{x}↔{T}\mathrm{Fne}{t}\right)$
41 40 cbvralvw ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{t}$
42 fnetg ${⊢}{T}\mathrm{Fne}{t}\to {T}\subseteq \mathrm{topGen}\left({t}\right)$
43 42 ralimi ${⊢}\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{t}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\subseteq \mathrm{topGen}\left({t}\right)$
44 41 43 sylbi ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\subseteq \mathrm{topGen}\left({t}\right)$
45 44 ad2antll ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to \forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\subseteq \mathrm{topGen}\left({t}\right)$
46 ssiin ${⊢}{T}\subseteq \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)↔\forall {t}\in {S}\phantom{\rule{.4em}{0ex}}{T}\subseteq \mathrm{topGen}\left({t}\right)$
47 45 46 sylibr ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {T}\subseteq \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)$
48 39 47 ssind ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {T}\subseteq 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)$
49 pwexg ${⊢}{X}\in {V}\to 𝒫{X}\in \mathrm{V}$
50 inex1g ${⊢}𝒫{X}\in \mathrm{V}\to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\in \mathrm{V}$
51 49 50 syl ${⊢}{X}\in {V}\to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\in \mathrm{V}$
52 51 ad2antrr ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\in \mathrm{V}$
53 bastg ${⊢}𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\in \mathrm{V}\to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\subseteq \mathrm{topGen}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
54 52 53 syl ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to 𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\subseteq \mathrm{topGen}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
55 48 54 sstrd ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {T}\subseteq \mathrm{topGen}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
56 22 12 isfne4 ${⊢}{T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)↔\left(\bigcup {T}=\bigcup \left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\wedge {T}\subseteq \mathrm{topGen}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
57 35 55 56 sylanbrc ${⊢}\left(\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\wedge \left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)\to {T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)$
58 57 ex ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left(\left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\to {T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)\right)$
59 32 58 impbid ${⊢}\left({X}\in {V}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}\right)\to \left({T}\mathrm{Fne}\left(𝒫{X}\cap \bigcap _{{t}\in {S}}\mathrm{topGen}\left({t}\right)\right)↔\left({X}=\bigcup {T}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{T}\mathrm{Fne}{x}\right)\right)$