Step | Hyp | Ref
| Expression |
1 | | fnerel 34863 |
. . 3
β’ Rel
Fne |
2 | 1 | brrelex2i 5693 |
. 2
β’ (π΄Fneπ΅ β π΅ β V) |
3 | | simpl 484 |
. . . . 5
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π = π) |
4 | | isfne.1 |
. . . . 5
β’ π = βͺ
π΄ |
5 | | isfne.2 |
. . . . 5
β’ π = βͺ
π΅ |
6 | 3, 4, 5 | 3eqtr3g 2796 |
. . . 4
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΄ = βͺ
π΅) |
7 | | fvex 6859 |
. . . . . . 7
β’
(topGenβπ΅)
β V |
8 | 7 | ssex 5282 |
. . . . . 6
β’ (π΄ β (topGenβπ΅) β π΄ β V) |
9 | 8 | adantl 483 |
. . . . 5
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π΄ β V) |
10 | 9 | uniexd 7683 |
. . . 4
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΄ β V) |
11 | 6, 10 | eqeltrrd 2835 |
. . 3
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΅ β V) |
12 | | uniexb 7702 |
. . 3
β’ (π΅ β V β βͺ π΅
β V) |
13 | 11, 12 | sylibr 233 |
. 2
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π΅ β V) |
14 | 4, 5 | isfne 34864 |
. . 3
β’ (π΅ β V β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) |
15 | | dfss3 3936 |
. . . . 5
β’ (π΄ β (topGenβπ΅) β βπ₯ β π΄ π₯ β (topGenβπ΅)) |
16 | | eltg 22330 |
. . . . . 6
β’ (π΅ β V β (π₯ β (topGenβπ΅) β π₯ β βͺ (π΅ β© π« π₯))) |
17 | 16 | ralbidv 3171 |
. . . . 5
β’ (π΅ β V β (βπ₯ β π΄ π₯ β (topGenβπ΅) β βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯))) |
18 | 15, 17 | bitrid 283 |
. . . 4
β’ (π΅ β V β (π΄ β (topGenβπ΅) β βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯))) |
19 | 18 | anbi2d 630 |
. . 3
β’ (π΅ β V β ((π = π β§ π΄ β (topGenβπ΅)) β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) |
20 | 14, 19 | bitr4d 282 |
. 2
β’ (π΅ β V β (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅)))) |
21 | 2, 13, 20 | pm5.21nii 380 |
1
β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) |