Metamath Proof Explorer

Theorem parhomcl2

Description: Variant of parhomcl . (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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parhomval.s ⊢ S ∈ V
parhomel.j ⊢ J ∈ V
parhomcl2.k ⊢ K = S ∪ J
parhomcl2.u ⊢ φ → U ∈ B
parhomcl2.v ⊢ φ → V ∈ B
parhomcl2.f ⊢ φ → F ∈ U H V
Assertion parhomcl2 ⊢ φ → F ∈ K

Proof

Step Hyp Ref Expression
1 parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parhomval.s ⊢ S ∈ V
3 parhomel.j ⊢ J ∈ V
4 parhomcl2.k ⊢ K = S ∪ J
5 parhomcl2.u ⊢ φ → U ∈ B
6 parhomcl2.v ⊢ φ → V ∈ B
7 parhomcl2.f ⊢ φ → F ∈ U H V
8 1 2 3 parhomel ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
9 5 6 8 syl2anc ⊢ φ → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
10 7 9 mpbid ⊢ φ → U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
11 3 elsn2 ⊢ F ∈ J ↔ F = J
12 11 bilanri ⊢ U = V ∧ F = J → F ∈ J
13 12 olcd ⊢ U = V ∧ F = J → F ∈ S ∨ F ∈ J
14 simprr ⊢ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → F ∈ S
15 14 orcd ⊢ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → F ∈ S ∨ F ∈ J
16 13 15 jaoi ⊢ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S → F ∈ S ∨ F ∈ J
17 10 16 syl ⊢ φ → F ∈ S ∨ F ∈ J
18 elun ⊢ F ∈ S ∪ J ↔ F ∈ S ∨ F ∈ J
19 17 18 sylibr ⊢ φ → F ∈ S ∪ J
20 19 4 eleqtrrdi ⊢ φ → F ∈ K