Metamath Proof Explorer

Theorem parhomco2

Description: Variant of parhomco . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses parhomval.h 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parhomeqor.f 
|- ( ph -> F e. ( U H V ) )
parhomeqor.g 
|- ( ph -> G e. ( V H W ) )
parhomco.p 
|- S C_ ~P J
parhomco2.s 
|- S e. _V
parhomco2.j 
|- J e. _V
parhomco2.n 
|- X =/= Y
parhomco2.u 
|- ( ph -> U e. B )
parhomco2.v 
|- ( ph -> V e. B )
parhomco2.w 
|- ( ph -> W e. B )
Assertion parhomco2 
|- ( ph -> ( G i^i F ) e. ( U H W ) )

Proof

Step Hyp Ref Expression
1 parhomval.h 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2 parhomeqor.f 
 |-  ( ph -> F e. ( U H V ) )
3 parhomeqor.g 
 |-  ( ph -> G e. ( V H W ) )
4 parhomco.p 
 |-  S C_ ~P J
5 parhomco2.s 
 |-  S e. _V
6 parhomco2.j 
 |-  J e. _V
7 parhomco2.n 
 |-  X =/= Y
8 parhomco2.u 
 |-  ( ph -> U e. B )
9 parhomco2.v 
 |-  ( ph -> V e. B )
10 parhomco2.w 
 |-  ( ph -> W e. B )
11 3 adantr 
 |-  ( ( ph /\ U = V ) -> G e. ( V H W ) )
12 2 adantr 
 |-  ( ( ph /\ U = V ) -> F e. ( U H V ) )
13 simpr 
 |-  ( ( ph /\ U = V ) -> U = V )
14 1 12 13 parhomideq 
 |-  ( ( ph /\ U = V ) -> F = J )
15 14 ineq2d 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = ( G i^i J ) )
16 1 4 3 parhomss 
 |-  ( ph -> G C_ J )
17 16 adantr 
 |-  ( ( ph /\ U = V ) -> G C_ J )
18 dfss2 
 |-  ( G C_ J <-> ( G i^i J ) = G )
19 17 18 sylib 
 |-  ( ( ph /\ U = V ) -> ( G i^i J ) = G )
20 15 19 eqtrd 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = G )
21 13 oveq1d 
 |-  ( ( ph /\ U = V ) -> ( U H W ) = ( V H W ) )
22 11 20 21 3eltr4d 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) e. ( U H W ) )
23 3 adantr 
 |-  ( ( ph /\ V = W ) -> G e. ( V H W ) )
24 simpr 
 |-  ( ( ph /\ V = W ) -> V = W )
25 1 23 24 parhomideq 
 |-  ( ( ph /\ V = W ) -> G = J )
26 25 ineq1d 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = ( J i^i F ) )
27 1 4 2 parhomss 
 |-  ( ph -> F C_ J )
28 27 adantr 
 |-  ( ( ph /\ V = W ) -> F C_ J )
29 sseqin2 
 |-  ( F C_ J <-> ( J i^i F ) = F )
30 28 29 sylib 
 |-  ( ( ph /\ V = W ) -> ( J i^i F ) = F )
31 26 30 eqtrd 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = F )
32 2 adantr 
 |-  ( ( ph /\ V = W ) -> F e. ( U H V ) )
33 24 oveq2d 
 |-  ( ( ph /\ V = W ) -> ( U H V ) = ( U H W ) )
34 32 33 eleqtrd 
 |-  ( ( ph /\ V = W ) -> F e. ( U H W ) )
35 31 34 eqeltrd 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) e. ( U H W ) )
36 1 2 3 parhomeqor 
 |-  ( ph -> ( U = V \/ V = W ) )
37 22 35 36 mpjaodan 
 |-  ( ph -> ( G i^i F ) e. ( U H W ) )