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 X V y S X = y T Fne 𝒫 X t S topGen t X = T x S T Fne x

Proof

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