| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ismred2.ss |
|- ( ph -> C C_ ~P X ) |
| 2 |
|
ismred2.in |
|- ( ( ph /\ s C_ C ) -> ( X i^i |^| s ) e. C ) |
| 3 |
|
eqid |
|- (/) = (/) |
| 4 |
|
rint0 |
|- ( (/) = (/) -> ( X i^i |^| (/) ) = X ) |
| 5 |
3 4
|
ax-mp |
|- ( X i^i |^| (/) ) = X |
| 6 |
|
0ss |
|- (/) C_ C |
| 7 |
|
0ex |
|- (/) e. _V |
| 8 |
|
sseq1 |
|- ( s = (/) -> ( s C_ C <-> (/) C_ C ) ) |
| 9 |
8
|
anbi2d |
|- ( s = (/) -> ( ( ph /\ s C_ C ) <-> ( ph /\ (/) C_ C ) ) ) |
| 10 |
|
inteq |
|- ( s = (/) -> |^| s = |^| (/) ) |
| 11 |
10
|
ineq2d |
|- ( s = (/) -> ( X i^i |^| s ) = ( X i^i |^| (/) ) ) |
| 12 |
11
|
eleq1d |
|- ( s = (/) -> ( ( X i^i |^| s ) e. C <-> ( X i^i |^| (/) ) e. C ) ) |
| 13 |
9 12
|
imbi12d |
|- ( s = (/) -> ( ( ( ph /\ s C_ C ) -> ( X i^i |^| s ) e. C ) <-> ( ( ph /\ (/) C_ C ) -> ( X i^i |^| (/) ) e. C ) ) ) |
| 14 |
7 13 2
|
vtocl |
|- ( ( ph /\ (/) C_ C ) -> ( X i^i |^| (/) ) e. C ) |
| 15 |
6 14
|
mpan2 |
|- ( ph -> ( X i^i |^| (/) ) e. C ) |
| 16 |
5 15
|
eqeltrrid |
|- ( ph -> X e. C ) |
| 17 |
|
simp2 |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s C_ C ) |
| 18 |
1
|
3ad2ant1 |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> C C_ ~P X ) |
| 19 |
17 18
|
sstrd |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s C_ ~P X ) |
| 20 |
|
simp3 |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s =/= (/) ) |
| 21 |
|
rintn0 |
|- ( ( s C_ ~P X /\ s =/= (/) ) -> ( X i^i |^| s ) = |^| s ) |
| 22 |
19 20 21
|
syl2anc |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> ( X i^i |^| s ) = |^| s ) |
| 23 |
2
|
3adant3 |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> ( X i^i |^| s ) e. C ) |
| 24 |
22 23
|
eqeltrrd |
|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> |^| s e. C ) |
| 25 |
1 16 24
|
ismred |
|- ( ph -> C e. ( Moore ` X ) ) |