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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parmapcl.f ⊢ φ → F ∈ U H V
parmapcl.i ⊢ φ → A ⁡ J = J
parmapcl.a ⊢ φ ∧ F ∈ S → A ⁡ F ∈ S
parmapcl2.s ⊢ S ∈ V
parmapcl2.j ⊢ J ∈ V
parmapcl2.u ⊢ φ → U ∈ B
parmapcl2.v ⊢ φ → V ∈ B
Assertion parmapcl2 ⊢ φ → A ⁡ F ∈ U H V

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parmapcl.f ⊢ φ → F ∈ U H V
3 parmapcl.i ⊢ φ → A ⁡ J = J
4 parmapcl.a ⊢ φ ∧ F ∈ S → A ⁡ F ∈ S
5 parmapcl2.s ⊢ S ∈ V
6 parmapcl2.j ⊢ J ∈ V
7 parmapcl2.u ⊢ φ → U ∈ B
8 parmapcl2.v ⊢ φ → V ∈ B
9 simprl ⊢ φ ∧ U = V ∧ F = J → U = V
10 simprr ⊢ φ ∧ U = V ∧ F = J → F = J
11 10 fveq2d ⊢ φ ∧ U = V ∧ F = J → A ⁡ F = A ⁡ J
12 3 adantr ⊢ φ ∧ U = V ∧ F = J → A ⁡ J = J
13 11 12 eqtrd ⊢ φ ∧ U = V ∧ F = J → A ⁡ F = J
14 9 13 jca ⊢ φ ∧ U = V ∧ F = J → U = V ∧ A ⁡ F = J
15 simprl ⊢ φ ∧ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → ¬ U = V
16 simprrl ⊢ φ ∧ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → U = X ∧ V = Y
17 simprrr ⊢ φ ∧ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → F ∈ S
18 17 4 syldan ⊢ φ ∧ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → A ⁡ F ∈ S
19 15 16 18 jca32 ⊢ φ ∧ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → ¬ U = V ∧ U = X ∧ V = Y ∧ A ⁡ F ∈ S
20 1 5 6 parhomel ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
21 7 8 20 syl2anc ⊢ φ → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
22 2 21 mpbid ⊢ φ → U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
23 14 19 22 orim12da ⊢ φ → U = V ∧ A ⁡ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ A ⁡ F ∈ S
24 1 5 6 parhomel ⊢ U ∈ B ∧ V ∈ B → A ⁡ F ∈ U H V ↔ U = V ∧ A ⁡ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ A ⁡ F ∈ S
25 7 8 24 syl2anc ⊢ φ → A ⁡ F ∈ U H V ↔ U = V ∧ A ⁡ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ A ⁡ F ∈ S
26 23 25 mpbird ⊢ φ → A ⁡ F ∈ U H V