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 ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
parmapcl2.s ⊢ 𝑆 ∈ V
parmapcl2.j ⊢ 𝐽 ∈ V
parmapcl2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
parmapcl2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion parmapcl2 ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2 parmapcl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3 parmapcl.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
4 parmapcl.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
5 parmapcl2.s ⊢ 𝑆 ∈ V
6 parmapcl2.j ⊢ 𝐽 ∈ V
7 parmapcl2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
8 parmapcl2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → 𝑈 = 𝑉 )
10 simprr ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → 𝐹 = 𝐽 )
11 10 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ 𝐽 ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
13 11 12 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → ( 𝐴 ‘ 𝐹 ) = 𝐽 )
14 9 13 jca ⊢ ( ( 𝜑 ∧ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ) → ( 𝑈 = 𝑉 ∧ ( 𝐴 ‘ 𝐹 ) = 𝐽 ) )
15 simprl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → ¬ 𝑈 = 𝑉 )
16 simprrl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )
17 simprrr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → 𝐹 ∈ 𝑆 )
18 17 4 syldan ⊢ ( ( 𝜑 ∧ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
19 15 16 18 jca32 ⊢ ( ( 𝜑 ∧ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) → ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 ) ) )
20 1 5 6 parhomel ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
21 7 8 20 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
22 2 21 mpbid ⊢ ( 𝜑 → ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) )
23 14 19 22 orim12da ⊢ ( 𝜑 → ( ( 𝑈 = 𝑉 ∧ ( 𝐴 ‘ 𝐹 ) = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 ) ) ) )
24 1 5 6 parhomel ⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ ( 𝐴 ‘ 𝐹 ) = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 ) ) ) ) )
25 7 8 24 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ ( 𝐴 ‘ 𝐹 ) = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 ) ) ) ) )
26 23 25 mpbird ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )