Metamath Proof Explorer

Theorem parhomco2

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

Proof

Step Hyp Ref Expression
1 parhomval.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2 parhomeqor.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3 parhomeqor.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
4 parhomco.p ⊢ 𝑆 ⊆ 𝒫 𝐽
5 parhomco2.s ⊢ 𝑆 ∈ V
6 parhomco2.j ⊢ 𝐽 ∈ V
7 parhomco2.n ⊢ 𝑋 ≠ 𝑌
8 parhomco2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
9 parhomco2.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
10 parhomco2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
14 1 12 13 parhomideq ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
15 14 ineq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐺 ∩ 𝐽 ) )
16 1 4 3 parhomss ⊢ ( 𝜑 → 𝐺 ⊆ 𝐽 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ⊆ 𝐽 )
18 dfss2 ⊢ ( 𝐺 ⊆ 𝐽 ↔ ( 𝐺 ∩ 𝐽 ) = 𝐺 )
19 17 18 sylib ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐽 ) = 𝐺 )
20 15 19 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = 𝐺 )
21 13 oveq1d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑈 𝐻 𝑊 ) = ( 𝑉 𝐻 𝑊 ) )
22 11 20 21 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )
23 3 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝑉 = 𝑊 )
25 1 23 24 parhomideq ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 = 𝐽 )
26 25 ineq1d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐽 ∩ 𝐹 ) )
27 1 4 2 parhomss ⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ⊆ 𝐽 )
29 sseqin2 ⊢ ( 𝐹 ⊆ 𝐽 ↔ ( 𝐽 ∩ 𝐹 ) = 𝐹 )
30 28 29 sylib ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ 𝐹 ) = 𝐹 )
31 26 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = 𝐹 )
32 2 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
33 24 oveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝑈 𝐻 𝑉 ) = ( 𝑈 𝐻 𝑊 ) )
34 32 33 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑊 ) )
35 31 34 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )
36 1 2 3 parhomeqor ⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )
37 22 35 36 mpjaodan ⊢ ( 𝜑 → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )