Step | Hyp | Ref
| Expression |
1 | | unitg 22691 |
. . . . . . . 8
β’ (π‘ β π β βͺ
(topGenβπ‘) = βͺ π‘) |
2 | 1 | adantl 481 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) = βͺ π‘) |
3 | | unieq 4919 |
. . . . . . . . . 10
β’ (π¦ = π‘ β βͺ π¦ = βͺ
π‘) |
4 | 3 | eqeq2d 2742 |
. . . . . . . . 9
β’ (π¦ = π‘ β (π = βͺ π¦ β π = βͺ π‘)) |
5 | 4 | rspccva 3611 |
. . . . . . . 8
β’
((βπ¦ β
π π = βͺ π¦ β§ π‘ β π) β π = βͺ π‘) |
6 | 5 | 3ad2antl2 1185 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π = βͺ π‘) |
7 | 2, 6 | eqtr4d 2774 |
. . . . . 6
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) = π) |
8 | | eqimss 4040 |
. . . . . 6
β’ (βͺ (topGenβπ‘) = π β βͺ
(topGenβπ‘) β
π) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) β
π) |
10 | | sspwuni 5103 |
. . . . 5
β’
((topGenβπ‘)
β π« π β
βͺ (topGenβπ‘) β π) |
11 | 9, 10 | sylibr 233 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β (topGenβπ‘) β π« π) |
12 | 11 | ralrimiva 3145 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π (topGenβπ‘) β π« π) |
13 | | ne0i 4334 |
. . . 4
β’ (π΄ β π β π β β
) |
14 | 13 | 3ad2ant3 1134 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π β β
) |
15 | | riinn0 5086 |
. . 3
β’
((βπ‘ β
π (topGenβπ‘) β π« π β§ π β β
) β (π« π β© β© π‘ β π (topGenβπ‘)) = β©
π‘ β π (topGenβπ‘)) |
16 | 12, 14, 15 | syl2anc 583 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (π« π β© β©
π‘ β π (topGenβπ‘)) = β©
π‘ β π (topGenβπ‘)) |
17 | | simp3 1137 |
. . . . . . . 8
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄ β π) |
18 | | ssid 4004 |
. . . . . . . 8
β’
(topGenβπ΄)
β (topGenβπ΄) |
19 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π‘ = π΄ β (topGenβπ‘) = (topGenβπ΄)) |
20 | 19 | sseq1d 4013 |
. . . . . . . . 9
β’ (π‘ = π΄ β ((topGenβπ‘) β (topGenβπ΄) β (topGenβπ΄) β (topGenβπ΄))) |
21 | 20 | rspcev 3612 |
. . . . . . . 8
β’ ((π΄ β π β§ (topGenβπ΄) β (topGenβπ΄)) β βπ‘ β π (topGenβπ‘) β (topGenβπ΄)) |
22 | 17, 18, 21 | sylancl 585 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π (topGenβπ‘) β (topGenβπ΄)) |
23 | | iinss 5059 |
. . . . . . 7
β’
(βπ‘ β
π (topGenβπ‘) β (topGenβπ΄) β β© π‘ β π (topGenβπ‘) β (topGenβπ΄)) |
24 | 22, 23 | syl 17 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β β©
π‘ β π (topGenβπ‘) β (topGenβπ΄)) |
25 | 24 | unissd 4918 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) β βͺ
(topGenβπ΄)) |
26 | | unitg 22691 |
. . . . . 6
β’ (π΄ β π β βͺ
(topGenβπ΄) = βͺ π΄) |
27 | 26 | 3ad2ant3 1134 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
(topGenβπ΄) = βͺ π΄) |
28 | 25, 27 | sseqtrd 4022 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) β βͺ π΄) |
29 | | unieq 4919 |
. . . . . . . . . . . . 13
β’ (π¦ = π΄ β βͺ π¦ = βͺ
π΄) |
30 | 29 | eqeq2d 2742 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (π = βͺ π¦ β π = βͺ π΄)) |
31 | 30 | rspccva 3611 |
. . . . . . . . . . 11
β’
((βπ¦ β
π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
32 | 31 | 3adant1 1129 |
. . . . . . . . . 10
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
33 | 32 | adantr 480 |
. . . . . . . . 9
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π = βͺ π΄) |
34 | 33, 6 | eqtr3d 2773 |
. . . . . . . 8
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π΄ = βͺ
π‘) |
35 | | simpr 484 |
. . . . . . . . 9
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π‘ β π) |
36 | | ssid 4004 |
. . . . . . . . 9
β’ π‘ β π‘ |
37 | | eltg3i 22685 |
. . . . . . . . 9
β’ ((π‘ β π β§ π‘ β π‘) β βͺ π‘ β (topGenβπ‘)) |
38 | 35, 36, 37 | sylancl 585 |
. . . . . . . 8
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π‘ β (topGenβπ‘)) |
39 | 34, 38 | eqeltrd 2832 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π΄ β (topGenβπ‘)) |
40 | 39 | ralrimiva 3145 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π βͺ π΄ β (topGenβπ‘)) |
41 | | uniexg 7734 |
. . . . . . . 8
β’ (π΄ β π β βͺ π΄ β V) |
42 | 41 | 3ad2ant3 1134 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β V) |
43 | | eliin 5002 |
. . . . . . 7
β’ (βͺ π΄
β V β (βͺ π΄ β β©
π‘ β π (topGenβπ‘) β βπ‘ β π βͺ π΄ β (topGenβπ‘))) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (βͺ π΄ β β© π‘ β π (topGenβπ‘) β βπ‘ β π βͺ π΄ β (topGenβπ‘))) |
45 | 40, 44 | mpbird 257 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β β© π‘ β π (topGenβπ‘)) |
46 | | elssuni 4941 |
. . . . 5
β’ (βͺ π΄
β β© π‘ β π (topGenβπ‘) β βͺ π΄ β βͺ β© π‘ β π (topGenβπ‘)) |
47 | 45, 46 | syl 17 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β βͺ β© π‘ β π (topGenβπ‘)) |
48 | 28, 47 | eqssd 3999 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) = βͺ π΄) |
49 | | eqid 2731 |
. . . 4
β’ βͺ β© π‘ β π (topGenβπ‘) = βͺ β© π‘ β π (topGenβπ‘) |
50 | | eqid 2731 |
. . . 4
β’ βͺ π΄ =
βͺ π΄ |
51 | 49, 50 | isfne4 35529 |
. . 3
β’ (β© π‘ β π (topGenβπ‘)Fneπ΄ β (βͺ
β© π‘ β π (topGenβπ‘) = βͺ π΄ β§ β© π‘ β π (topGenβπ‘) β (topGenβπ΄))) |
52 | 48, 24, 51 | sylanbrc 582 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β β©
π‘ β π (topGenβπ‘)Fneπ΄) |
53 | 16, 52 | eqbrtrd 5170 |
1
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (π« π β© β©
π‘ β π (topGenβπ‘))Fneπ΄) |