Step | Hyp | Ref
| Expression |
1 | | fnerel 35218 |
. . 3
β’ Rel
Fne |
2 | 1 | brrelex2i 5733 |
. 2
β’ (π΄Fneπ΅ β π΅ β V) |
3 | | simpl 483 |
. . . . 5
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π = π) |
4 | | isfne.1 |
. . . . 5
β’ π = βͺ
π΄ |
5 | | isfne.2 |
. . . . 5
β’ π = βͺ
π΅ |
6 | 3, 4, 5 | 3eqtr3g 2795 |
. . . 4
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΄ = βͺ
π΅) |
7 | | fvex 6904 |
. . . . . . 7
β’
(topGenβπ΅)
β V |
8 | 7 | ssex 5321 |
. . . . . 6
β’ (π΄ β (topGenβπ΅) β π΄ β V) |
9 | 8 | adantl 482 |
. . . . 5
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π΄ β V) |
10 | 9 | uniexd 7731 |
. . . 4
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΄ β V) |
11 | 6, 10 | eqeltrrd 2834 |
. . 3
β’ ((π = π β§ π΄ β (topGenβπ΅)) β βͺ π΅ β V) |
12 | | uniexb 7750 |
. . 3
β’ (π΅ β V β βͺ π΅
β V) |
13 | 11, 12 | sylibr 233 |
. 2
β’ ((π = π β§ π΄ β (topGenβπ΅)) β π΅ β V) |
14 | 4, 5 | isfne 35219 |
. . 3
β’ (π΅ β V β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) |
15 | | dfss3 3970 |
. . . . 5
β’ (π΄ β (topGenβπ΅) β βπ₯ β π΄ π₯ β (topGenβπ΅)) |
16 | | eltg 22459 |
. . . . . 6
β’ (π΅ β V β (π₯ β (topGenβπ΅) β π₯ β βͺ (π΅ β© π« π₯))) |
17 | 16 | ralbidv 3177 |
. . . . 5
β’ (π΅ β V β (βπ₯ β π΄ π₯ β (topGenβπ΅) β βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯))) |
18 | 15, 17 | bitrid 282 |
. . . 4
β’ (π΅ β V β (π΄ β (topGenβπ΅) β βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯))) |
19 | 18 | anbi2d 629 |
. . 3
β’ (π΅ β V β ((π = π β§ π΄ β (topGenβπ΅)) β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) |
20 | 14, 19 | bitr4d 281 |
. 2
β’ (π΅ β V β (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅)))) |
21 | 2, 13, 20 | pm5.21nii 379 |
1
β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) |