Metamath Proof Explorer

Theorem parmapco2

Description: Variant of parmapco . (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 ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
parmapco2.s ⊢ 𝑆 ∈ V
parmapco2.j ⊢ 𝐽 ∈ V
parmapco2.p ⊢ 𝑆 ⊆ 𝒫 𝐽
parmapco2.n ⊢ 𝑋 ≠ 𝑌
parmapco2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
parmapco2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
parmapco2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
parmapco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
parmapco2.b ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐺 ) ∈ 𝑆 )
Assertion parmapco2 ( 𝜑 → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2 parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3 parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
4 parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
5 parmapco2.s ⊢ 𝑆 ∈ V
6 parmapco2.j ⊢ 𝐽 ∈ V
7 parmapco2.p ⊢ 𝑆 ⊆ 𝒫 𝐽
8 parmapco2.n ⊢ 𝑋 ≠ 𝑌
9 parmapco2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
10 parmapco2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
11 parmapco2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
12 parmapco2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
13 parmapco2.b ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐺 ) ∈ 𝑆 )
14 1 12 3 13 parmapcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐺 ) ∈ ( 𝑉 𝐻 𝑊 ) )
15 1 7 14 parhomss ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 )
17 dfss2 ⊢ ( ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 ↔ ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) = ( 𝐴 ‘ 𝐺 ) )
18 16 17 sylib ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) = ( 𝐴 ‘ 𝐺 ) )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
21 1 19 20 parhomideq ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ 𝐽 ) )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
24 22 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = 𝐽 )
25 24 ineq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) )
26 21 ineq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐺 ∩ 𝐽 ) )
27 1 7 12 parhomss ⊢ ( 𝜑 → 𝐺 ⊆ 𝐽 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ⊆ 𝐽 )
29 dfss2 ⊢ ( 𝐺 ⊆ 𝐽 ↔ ( 𝐺 ∩ 𝐽 ) = 𝐺 )
30 28 29 sylib ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐽 ) = 𝐺 )
31 26 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = 𝐺 )
32 31 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( 𝐴 ‘ 𝐺 ) )
33 18 25 32 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )
34 1 2 3 4 parmapcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )
35 1 7 34 parhomss ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 )
37 sseqin2 ⊢ ( ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 ↔ ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
38 36 37 sylib ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
39 12 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝑉 = 𝑊 )
41 1 39 40 parhomideq ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 = 𝐽 )
42 41 fveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐺 ) = ( 𝐴 ‘ 𝐽 ) )
43 3 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
44 42 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐺 ) = 𝐽 )
45 44 ineq1d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) )
46 41 ineq1d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐽 ∩ 𝐹 ) )
47 1 7 2 parhomss ⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ⊆ 𝐽 )
49 sseqin2 ⊢ ( 𝐹 ⊆ 𝐽 ↔ ( 𝐽 ∩ 𝐹 ) = 𝐹 )
50 48 49 sylib ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ 𝐹 ) = 𝐹 )
51 46 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = 𝐹 )
52 51 fveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
53 38 45 52 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )
54 1 2 12 parhomeqor ⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )
55 33 53 54 mpjaodan ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )