Step | Hyp | Ref
| Expression |
1 | | riin0 5047 |
. . . . . . . . . 10
β’ (π = β
β (π«
π β© β© π‘ β π (topGenβπ‘)) = π« π) |
2 | 1 | unieqd 4884 |
. . . . . . . . 9
β’ (π = β
β βͺ (π« π β© β©
π‘ β π (topGenβπ‘)) = βͺ π«
π) |
3 | | unipw 5412 |
. . . . . . . . 9
β’ βͺ π« π = π |
4 | 2, 3 | eqtr2di 2794 |
. . . . . . . 8
β’ (π = β
β π = βͺ
(π« π β© β© π‘ β π (topGenβπ‘))) |
5 | 4 | a1i 11 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (π = β
β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘)))) |
6 | | n0 4311 |
. . . . . . . 8
β’ (π β β
β
βπ₯ π₯ β π) |
7 | | unieq 4881 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β βͺ π¦ = βͺ
π₯) |
8 | 7 | eqeq2d 2748 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (π = βͺ π¦ β π = βͺ π₯)) |
9 | 8 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ¦ β
π π = βͺ π¦ β§ π₯ β π) β π = βͺ π₯) |
10 | 9 | 3adant1 1131 |
. . . . . . . . . . 11
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π₯ β π) β π = βͺ π₯) |
11 | | fnemeet1 34867 |
. . . . . . . . . . . 12
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π₯ β π) β (π« π β© β©
π‘ β π (topGenβπ‘))Fneπ₯) |
12 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ (π« π β© β©
π‘ β π (topGenβπ‘)) = βͺ (π«
π β© β© π‘ β π (topGenβπ‘)) |
13 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ π₯ =
βͺ π₯ |
14 | 12, 13 | fnebas 34845 |
. . . . . . . . . . . 12
β’
((π« π β©
β© π‘ β π (topGenβπ‘))Fneπ₯ β βͺ
(π« π β© β© π‘ β π (topGenβπ‘)) = βͺ π₯) |
15 | 11, 14 | syl 17 |
. . . . . . . . . . 11
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π₯ β π) β βͺ
(π« π β© β© π‘ β π (topGenβπ‘)) = βͺ π₯) |
16 | 10, 15 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π₯ β π) β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘))) |
17 | 16 | 3expia 1122 |
. . . . . . . . 9
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (π₯ β π β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘)))) |
18 | 17 | exlimdv 1937 |
. . . . . . . 8
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (βπ₯ π₯ β π β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘)))) |
19 | 6, 18 | biimtrid 241 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (π β β
β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘)))) |
20 | 5, 19 | pm2.61dne 3032 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘))) |
21 | 20 | adantr 482 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ πFne(π« π β© β©
π‘ β π (topGenβπ‘))) β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘))) |
22 | | eqid 2737 |
. . . . . . 7
β’ βͺ π =
βͺ π |
23 | 22, 12 | fnebas 34845 |
. . . . . 6
β’ (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β βͺ π = βͺ
(π« π β© β© π‘ β π (topGenβπ‘))) |
24 | 23 | adantl 483 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ πFne(π« π β© β©
π‘ β π (topGenβπ‘))) β βͺ π = βͺ
(π« π β© β© π‘ β π (topGenβπ‘))) |
25 | 21, 24 | eqtr4d 2780 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ πFne(π« π β© β©
π‘ β π (topGenβπ‘))) β π = βͺ π) |
26 | 25 | ex 414 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β π = βͺ π)) |
27 | | fnetr 34852 |
. . . . . . 7
β’ ((πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β§ (π« π β© β©
π‘ β π (topGenβπ‘))Fneπ₯) β πFneπ₯) |
28 | 27 | expcom 415 |
. . . . . 6
β’
((π« π β©
β© π‘ β π (topGenβπ‘))Fneπ₯ β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β πFneπ₯)) |
29 | 11, 28 | syl 17 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π₯ β π) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β πFneπ₯)) |
30 | 29 | 3expa 1119 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ π₯ β π) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β πFneπ₯)) |
31 | 30 | ralrimdva 3152 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β βπ₯ β π πFneπ₯)) |
32 | 26, 31 | jcad 514 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β (π = βͺ π β§ βπ₯ β π πFneπ₯))) |
33 | | simprl 770 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π = βͺ π) |
34 | 20 | adantr 482 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π = βͺ (π«
π β© β© π‘ β π (topGenβπ‘))) |
35 | 33, 34 | eqtr3d 2779 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β βͺ π = βͺ
(π« π β© β© π‘ β π (topGenβπ‘))) |
36 | | eqimss2 4006 |
. . . . . . . 8
β’ (π = βͺ
π β βͺ π
β π) |
37 | 36 | ad2antrl 727 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β βͺ π β π) |
38 | | sspwuni 5065 |
. . . . . . 7
β’ (π β π« π β βͺ π
β π) |
39 | 37, 38 | sylibr 233 |
. . . . . 6
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π β π« π) |
40 | | breq2 5114 |
. . . . . . . . . 10
β’ (π₯ = π‘ β (πFneπ₯ β πFneπ‘)) |
41 | 40 | cbvralvw 3228 |
. . . . . . . . 9
β’
(βπ₯ β
π πFneπ₯ β βπ‘ β π πFneπ‘) |
42 | | fnetg 34846 |
. . . . . . . . . 10
β’ (πFneπ‘ β π β (topGenβπ‘)) |
43 | 42 | ralimi 3087 |
. . . . . . . . 9
β’
(βπ‘ β
π πFneπ‘ β βπ‘ β π π β (topGenβπ‘)) |
44 | 41, 43 | sylbi 216 |
. . . . . . . 8
β’
(βπ₯ β
π πFneπ₯ β βπ‘ β π π β (topGenβπ‘)) |
45 | 44 | ad2antll 728 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β βπ‘ β π π β (topGenβπ‘)) |
46 | | ssiin 5020 |
. . . . . . 7
β’ (π β β© π‘ β π (topGenβπ‘) β βπ‘ β π π β (topGenβπ‘)) |
47 | 45, 46 | sylibr 233 |
. . . . . 6
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π β β©
π‘ β π (topGenβπ‘)) |
48 | 39, 47 | ssind 4197 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π β (π« π β© β©
π‘ β π (topGenβπ‘))) |
49 | | pwexg 5338 |
. . . . . . . 8
β’ (π β π β π« π β V) |
50 | | inex1g 5281 |
. . . . . . . 8
β’
(π« π β
V β (π« π β©
β© π‘ β π (topGenβπ‘)) β V) |
51 | 49, 50 | syl 17 |
. . . . . . 7
β’ (π β π β (π« π β© β©
π‘ β π (topGenβπ‘)) β V) |
52 | 51 | ad2antrr 725 |
. . . . . 6
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β (π« π β© β©
π‘ β π (topGenβπ‘)) β V) |
53 | | bastg 22332 |
. . . . . 6
β’
((π« π β©
β© π‘ β π (topGenβπ‘)) β V β (π« π β© β© π‘ β π (topGenβπ‘)) β (topGenβ(π« π β© β© π‘ β π (topGenβπ‘)))) |
54 | 52, 53 | syl 17 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β (π« π β© β©
π‘ β π (topGenβπ‘)) β (topGenβ(π« π β© β© π‘ β π (topGenβπ‘)))) |
55 | 48, 54 | sstrd 3959 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β π β (topGenβ(π« π β© β© π‘ β π (topGenβπ‘)))) |
56 | 22, 12 | isfne4 34841 |
. . . 4
β’ (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β (βͺ π = βͺ
(π« π β© β© π‘ β π (topGenβπ‘)) β§ π β (topGenβ(π« π β© β© π‘ β π (topGenβπ‘))))) |
57 | 35, 55, 56 | sylanbrc 584 |
. . 3
β’ (((π β π β§ βπ¦ β π π = βͺ π¦) β§ (π = βͺ π β§ βπ₯ β π πFneπ₯)) β πFne(π« π β© β©
π‘ β π (topGenβπ‘))) |
58 | 57 | ex 414 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β ((π = βͺ π β§ βπ₯ β π πFneπ₯) β πFne(π« π β© β©
π‘ β π (topGenβπ‘)))) |
59 | 32, 58 | impbid 211 |
1
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (πFne(π« π β© β©
π‘ β π (topGenβπ‘)) β (π = βͺ π β§ βπ₯ β π πFneπ₯))) |