| Step |
Hyp |
Ref |
Expression |
| 1 |
|
inopn |
|- ( ( J e. Top /\ x e. J /\ y e. J ) -> ( x i^i y ) e. J ) |
| 2 |
1
|
3expb |
|- ( ( J e. Top /\ ( x e. J /\ y e. J ) ) -> ( x i^i y ) e. J ) |
| 3 |
|
simpr |
|- ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> z e. ( x i^i y ) ) |
| 4 |
|
ssid |
|- ( x i^i y ) C_ ( x i^i y ) |
| 5 |
3 4
|
jctir |
|- ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) |
| 6 |
|
eleq2 |
|- ( w = ( x i^i y ) -> ( z e. w <-> z e. ( x i^i y ) ) ) |
| 7 |
|
sseq1 |
|- ( w = ( x i^i y ) -> ( w C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) ) |
| 8 |
6 7
|
anbi12d |
|- ( w = ( x i^i y ) -> ( ( z e. w /\ w C_ ( x i^i y ) ) <-> ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) ) |
| 9 |
8
|
rspcev |
|- ( ( ( x i^i y ) e. J /\ ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) |
| 10 |
2 5 9
|
syl2an2r |
|- ( ( ( J e. Top /\ ( x e. J /\ y e. J ) ) /\ z e. ( x i^i y ) ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) |
| 11 |
10
|
exp31 |
|- ( J e. Top -> ( ( x e. J /\ y e. J ) -> ( z e. ( x i^i y ) -> E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) ) ) |
| 12 |
11
|
ralrimdv |
|- ( J e. Top -> ( ( x e. J /\ y e. J ) -> A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) ) |
| 13 |
12
|
ralrimivv |
|- ( J e. Top -> A. x e. J A. y e. J A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) |
| 14 |
|
isbasis2g |
|- ( J e. Top -> ( J e. TopBases <-> A. x e. J A. y e. J A. z e. ( x i^i y ) E. w e. J ( z e. w /\ w C_ ( x i^i y ) ) ) ) |
| 15 |
13 14
|
mpbird |
|- ( J e. Top -> J e. TopBases ) |