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 simpr 
 |-  ( ( ph /\ y ( ~=ph ` J ) x ) -> y ( ~=ph ` J ) x )
10 isphtpc 
 |-  ( y ( ~=ph ` J ) x <-> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
11 9 10 sylib 
 |-  ( ( ph /\ y ( ~=ph ` J ) x ) -> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
12 11 adantrl 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
13 12 simp2d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> x e. ( II Cn J ) )
14 phtpc01 
 |-  ( y ( ~=ph ` J ) x -> ( ( y ` 0 ) = ( x ` 0 ) /\ ( y ` 1 ) = ( x ` 1 ) ) )
15 14 ad2antll 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( ( y ` 0 ) = ( x ` 0 ) /\ ( y ` 1 ) = ( x ` 1 ) ) )
16 15 simpld 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 0 ) = ( x ` 0 ) )
17 4 2 3 6 om1elbas 
 |-  ( ph -> ( y e. K <-> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) ) )
18 17 biimpa 
 |-  ( ( ph /\ y e. K ) -> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) )
19 18 adantrr 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) )
20 19 simp2d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 0 ) = Y )
21 16 20 eqtr3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x ` 0 ) = Y )
22 15 simprd 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 1 ) = ( x ` 1 ) )
23 19 simp3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( y ` 1 ) = Y )
24 22 23 eqtr3d 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x ` 1 ) = Y )
25 4 2 3 6 om1elbas 
 |-  ( ph -> ( x e. K <-> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) ) )
26 25 adantr 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> ( x e. K <-> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) ) )
27 13 21 24 26 mpbir3and 
 |-  ( ( ph /\ ( y e. K /\ y ( ~=ph ` J ) x ) ) -> x e. K )
28 27 rexlimdvaa 
 |-  ( ph -> ( E. y e. K y ( ~=ph ` J ) x -> x e. K ) )
29 8 28 syl5bi 
 |-  ( ph -> ( x e. ( ( ~=ph ` J ) " K ) -> x e. K ) )
30 29 ssrdv 
 |-  ( ph -> ( ( ~=ph ` J ) " K ) C_ K )
31 simp1 
 |-  ( ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) -> x e. ( II Cn J ) )
32 25 31 syl6bi 
 |-  ( ph -> ( x e. K -> x e. ( II Cn J ) ) )
33 32 ssrdv 
 |-  ( ph -> K C_ ( II Cn J ) )
34 30 33 jca 
 |-  ( ph -> ( ( ( ~=ph ` J ) " K ) C_ K /\ K C_ ( II Cn J ) ) )