Metamath Proof Explorer

Theorem parmapcl2

Description: Variant of parmapcl . (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 parmapcl.h 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parmapcl.f 
|- ( ph -> F e. ( U H V ) )
parmapcl.i 
|- ( ph -> ( A ` J ) = J )
parmapcl.a 
|- ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
parmapcl2.s 
|- S e. _V
parmapcl2.j 
|- J e. _V
parmapcl2.u 
|- ( ph -> U e. B )
parmapcl2.v 
|- ( ph -> V e. B )
Assertion parmapcl2 
|- ( ph -> ( A ` F ) e. ( U H V ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2 parmapcl.f 
 |-  ( ph -> F e. ( U H V ) )
3 parmapcl.i 
 |-  ( ph -> ( A ` J ) = J )
4 parmapcl.a 
 |-  ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
5 parmapcl2.s 
 |-  S e. _V
6 parmapcl2.j 
 |-  J e. _V
7 parmapcl2.u 
 |-  ( ph -> U e. B )
8 parmapcl2.v 
 |-  ( ph -> V e. B )
9 simprl 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> U = V )
10 simprr 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> F = J )
11 10 fveq2d 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> ( A ` F ) = ( A ` J ) )
12 3 adantr 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> ( A ` J ) = J )
13 11 12 eqtrd 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> ( A ` F ) = J )
14 9 13 jca 
 |-  ( ( ph /\ ( U = V /\ F = J ) ) -> ( U = V /\ ( A ` F ) = J ) )
15 simprl 
 |-  ( ( ph /\ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> -. U = V )
16 simprrl 
 |-  ( ( ph /\ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> ( U = X /\ V = Y ) )
17 simprrr 
 |-  ( ( ph /\ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> F e. S )
18 17 4 syldan 
 |-  ( ( ph /\ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> ( A ` F ) e. S )
19 15 16 18 jca32 
 |-  ( ( ph /\ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) -> ( -. U = V /\ ( ( U = X /\ V = Y ) /\ ( A ` F ) e. S ) ) )
20 1 5 6 parhomel 
 |-  ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
21 7 8 20 syl2anc 
 |-  ( ph -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
22 2 21 mpbid 
 |-  ( ph -> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) )
23 14 19 22 orim12da 
 |-  ( ph -> ( ( U = V /\ ( A ` F ) = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ ( A ` F ) e. S ) ) ) )
24 1 5 6 parhomel 
 |-  ( ( U e. B /\ V e. B ) -> ( ( A ` F ) e. ( U H V ) <-> ( ( U = V /\ ( A ` F ) = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ ( A ` F ) e. S ) ) ) ) )
25 7 8 24 syl2anc 
 |-  ( ph -> ( ( A ` F ) e. ( U H V ) <-> ( ( U = V /\ ( A ` F ) = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ ( A ` F ) e. S ) ) ) ) )
26 23 25 mpbird 
 |-  ( ph -> ( A ` F ) e. ( U H V ) )