Step | Hyp | Ref
| Expression |
1 | | unitg 22690 |
. . . . . . . 8
β’ (π‘ β π β βͺ
(topGenβπ‘) = βͺ π‘) |
2 | 1 | adantl 480 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) = βͺ π‘) |
3 | | unieq 4918 |
. . . . . . . . . 10
β’ (π¦ = π‘ β βͺ π¦ = βͺ
π‘) |
4 | 3 | eqeq2d 2741 |
. . . . . . . . 9
β’ (π¦ = π‘ β (π = βͺ π¦ β π = βͺ π‘)) |
5 | 4 | rspccva 3610 |
. . . . . . . 8
β’
((βπ¦ β
π π = βͺ π¦ β§ π‘ β π) β π = βͺ π‘) |
6 | 5 | 3ad2antl2 1184 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π = βͺ π‘) |
7 | 2, 6 | eqtr4d 2773 |
. . . . . 6
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) = π) |
8 | | eqimss 4039 |
. . . . . 6
β’ (βͺ (topGenβπ‘) = π β βͺ
(topGenβπ‘) β
π) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ
(topGenβπ‘) β
π) |
10 | | sspwuni 5102 |
. . . . 5
β’
((topGenβπ‘)
β π« π β
βͺ (topGenβπ‘) β π) |
11 | 9, 10 | sylibr 233 |
. . . 4
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β (topGenβπ‘) β π« π) |
12 | 11 | ralrimiva 3144 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π (topGenβπ‘) β π« π) |
13 | | ne0i 4333 |
. . . 4
β’ (π΄ β π β π β β
) |
14 | 13 | 3ad2ant3 1133 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π β β
) |
15 | | riinn0 5085 |
. . 3
β’
((βπ‘ β
π (topGenβπ‘) β π« π β§ π β β
) β (π« π β© β© π‘ β π (topGenβπ‘)) = β©
π‘ β π (topGenβπ‘)) |
16 | 12, 14, 15 | syl2anc 582 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (π« π β© β©
π‘ β π (topGenβπ‘)) = β©
π‘ β π (topGenβπ‘)) |
17 | | simp3 1136 |
. . . . . . . 8
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄ β π) |
18 | | ssid 4003 |
. . . . . . . 8
β’
(topGenβπ΄)
β (topGenβπ΄) |
19 | | fveq2 6890 |
. . . . . . . . . 10
β’ (π‘ = π΄ β (topGenβπ‘) = (topGenβπ΄)) |
20 | 19 | sseq1d 4012 |
. . . . . . . . 9
β’ (π‘ = π΄ β ((topGenβπ‘) β (topGenβπ΄) β (topGenβπ΄) β (topGenβπ΄))) |
21 | 20 | rspcev 3611 |
. . . . . . . 8
β’ ((π΄ β π β§ (topGenβπ΄) β (topGenβπ΄)) β βπ‘ β π (topGenβπ‘) β (topGenβπ΄)) |
22 | 17, 18, 21 | sylancl 584 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π (topGenβπ‘) β (topGenβπ΄)) |
23 | | iinss 5058 |
. . . . . . 7
β’
(βπ‘ β
π (topGenβπ‘) β (topGenβπ΄) β β© π‘ β π (topGenβπ‘) β (topGenβπ΄)) |
24 | 22, 23 | syl 17 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β β©
π‘ β π (topGenβπ‘) β (topGenβπ΄)) |
25 | 24 | unissd 4917 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) β βͺ
(topGenβπ΄)) |
26 | | unitg 22690 |
. . . . . 6
β’ (π΄ β π β βͺ
(topGenβπ΄) = βͺ π΄) |
27 | 26 | 3ad2ant3 1133 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
(topGenβπ΄) = βͺ π΄) |
28 | 25, 27 | sseqtrd 4021 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) β βͺ π΄) |
29 | | unieq 4918 |
. . . . . . . . . . . . 13
β’ (π¦ = π΄ β βͺ π¦ = βͺ
π΄) |
30 | 29 | eqeq2d 2741 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (π = βͺ π¦ β π = βͺ π΄)) |
31 | 30 | rspccva 3610 |
. . . . . . . . . . 11
β’
((βπ¦ β
π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
32 | 31 | 3adant1 1128 |
. . . . . . . . . 10
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π = βͺ π΄) |
33 | 32 | adantr 479 |
. . . . . . . . 9
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π = βͺ π΄) |
34 | 33, 6 | eqtr3d 2772 |
. . . . . . . 8
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π΄ = βͺ
π‘) |
35 | | simpr 483 |
. . . . . . . . 9
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β π‘ β π) |
36 | | ssid 4003 |
. . . . . . . . 9
β’ π‘ β π‘ |
37 | | eltg3i 22684 |
. . . . . . . . 9
β’ ((π‘ β π β§ π‘ β π‘) β βͺ π‘ β (topGenβπ‘)) |
38 | 35, 36, 37 | sylancl 584 |
. . . . . . . 8
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π‘ β (topGenβπ‘)) |
39 | 34, 38 | eqeltrd 2831 |
. . . . . . 7
β’ (((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β§ π‘ β π) β βͺ π΄ β (topGenβπ‘)) |
40 | 39 | ralrimiva 3144 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βπ‘ β π βͺ π΄ β (topGenβπ‘)) |
41 | | uniexg 7732 |
. . . . . . . 8
β’ (π΄ β π β βͺ π΄ β V) |
42 | 41 | 3ad2ant3 1133 |
. . . . . . 7
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β V) |
43 | | eliin 5001 |
. . . . . . 7
β’ (βͺ π΄
β V β (βͺ π΄ β β©
π‘ β π (topGenβπ‘) β βπ‘ β π βͺ π΄ β (topGenβπ‘))) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (βͺ π΄ β β© π‘ β π (topGenβπ‘) β βπ‘ β π βͺ π΄ β (topGenβπ‘))) |
45 | 40, 44 | mpbird 256 |
. . . . 5
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β β© π‘ β π (topGenβπ‘)) |
46 | | elssuni 4940 |
. . . . 5
β’ (βͺ π΄
β β© π‘ β π (topGenβπ‘) β βͺ π΄ β βͺ β© π‘ β π (topGenβπ‘)) |
47 | 45, 46 | syl 17 |
. . . 4
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ π΄ β βͺ β© π‘ β π (topGenβπ‘)) |
48 | 28, 47 | eqssd 3998 |
. . 3
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β βͺ
β© π‘ β π (topGenβπ‘) = βͺ π΄) |
49 | | eqid 2730 |
. . . 4
β’ βͺ β© π‘ β π (topGenβπ‘) = βͺ β© π‘ β π (topGenβπ‘) |
50 | | eqid 2730 |
. . . 4
β’ βͺ π΄ =
βͺ π΄ |
51 | 49, 50 | isfne4 35528 |
. . 3
β’ (β© π‘ β π (topGenβπ‘)Fneπ΄ β (βͺ
β© π‘ β π (topGenβπ‘) = βͺ π΄ β§ β© π‘ β π (topGenβπ‘) β (topGenβπ΄))) |
52 | 48, 24, 51 | sylanbrc 581 |
. 2
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β β©
π‘ β π (topGenβπ‘)Fneπ΄) |
53 | 16, 52 | eqbrtrd 5169 |
1
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (π« π β© β©
π‘ β π (topGenβπ‘))Fneπ΄) |