Metamath Proof Explorer

Theorem pi1blem

Description: Lemma for pi1buni . (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g 
|- G = ( J pi1 Y )
pi1val.1 
|- ( ph -> J e. ( TopOn ` X ) )
pi1val.2 
|- ( ph -> Y e. X )
pi1val.o 
|- O = ( J Om1 Y )
pi1bas.b 
|- ( ph -> B = ( Base ` G ) )
pi1bas.k 
|- ( ph -> K = ( Base ` O ) )
Assertion pi1blem 
|- ( ph -> ( ( ( ~=ph ` J ) " K ) C_ K /\ K C_ ( II Cn J ) ) )

Proof

Step Hyp Ref Expression
1 pi1val.g 
 |-  G = ( J pi1 Y )
2 pi1val.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 pi1val.2 
 |-  ( ph -> Y e. X )
4 pi1val.o 
 |-  O = ( J Om1 Y )
5 pi1bas.b 
 |-  ( ph -> B = ( Base ` G ) )
6 pi1bas.k 
 |-  ( ph -> K = ( Base ` O ) )
7 vex 
 |-  x e. _V
8 7 elima 
 |-  ( x e. ( ( ~=ph ` J ) " K ) <-> E. y e. K y ( ~=ph ` J ) x )
9 isphtpc 
 |-  ( y ( ~=ph ` J ) x <-> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
10 9 bilani 
 |-  ( ( ph /\ y ( ~=ph ` J ) x ) -> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
11 10 adantrl 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
12 11 simp2d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> x e. ( II Cn J ) )
13 phtpc01 
 |-  ( y ( ~=ph ` J ) x -> ( ( y ` 0 ) = ( x ` 0 ) /\ ( y ` 1 ) = ( x ` 1 ) ) )
14 13 ad2antll 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( ( y ` 0 ) = ( x ` 0 ) /\ ( y ` 1 ) = ( x ` 1 ) ) )
15 14 simpld 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 0 ) = ( x ` 0 ) )
16 4 2 3 6 om1elbas 
 |-  ( ph -> ( y e. K <-> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) ) )
17 16 biimpa 
 |-  ( ( ph /\ y e. K ) -> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) )
18 17 adantrr 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) )
19 18 simp2d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 0 ) = Y )
20 15 19 eqtr3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x ` 0 ) = Y )
21 14 simprd 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 1 ) = ( x ` 1 ) )
22 18 simp3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 1 ) = Y )
23 21 22 eqtr3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x ` 1 ) = Y )
24 4 2 3 6 om1elbas 
 |-  ( ph -> ( x e. K <-> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) ) )
25 24 adantr 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x e. K <-> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) ) )
26 12 20 23 25 mpbir3and 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> x e. K )
27 26 rexlimdvaa 
 |-  ( ph -> ( E. y e. K y ( ~=ph ` J ) x -> x e. K ) )
28 8 27 biimtrid 
 |-  ( ph -> ( x e. ( ( ~=ph ` J ) " K ) -> x e. K ) )
29 28 ssrdv 
 |-  ( ph -> ( ( ~=ph ` J ) " K ) C_ K )
30 simp1 
 |-  ( ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) -> x e. ( II Cn J ) )
31 24 30 biimtrdi 
 |-  ( ph -> ( x e. K -> x e. ( II Cn J ) ) )
32 31 ssrdv 
 |-  ( ph -> K C_ ( II Cn J ) )
33 29 32 jca 
 |-  ( ph -> ( ( ( ~=ph ` J ) " K ) C_ K /\ K C_ ( II Cn J ) ) )