Step |
Hyp |
Ref |
Expression |
1 |
|
tgqioo2.1 |
|- J = ( topGen ` ran (,) ) |
2 |
|
tgqioo2.2 |
|- ( ph -> A e. J ) |
3 |
|
eqid |
|- ( topGen ` ( (,) " ( QQ X. QQ ) ) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) |
4 |
3
|
tgqioo |
|- ( topGen ` ran (,) ) = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) |
5 |
1 4 3
|
3eqtri |
|- J = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) |
6 |
5
|
a1i |
|- ( ph -> J = ( topGen ` ( (,) " ( QQ X. QQ ) ) ) ) |
7 |
2 6
|
eleqtrd |
|- ( ph -> A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) ) |
8 |
|
iooex |
|- (,) e. _V |
9 |
|
imaexg |
|- ( (,) e. _V -> ( (,) " ( QQ X. QQ ) ) e. _V ) |
10 |
8 9
|
ax-mp |
|- ( (,) " ( QQ X. QQ ) ) e. _V |
11 |
|
eltg3 |
|- ( ( (,) " ( QQ X. QQ ) ) e. _V -> ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) ) ) |
12 |
10 11
|
ax-mp |
|- ( A e. ( topGen ` ( (,) " ( QQ X. QQ ) ) ) <-> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) ) |
13 |
7 12
|
sylib |
|- ( ph -> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) ) |