Metamath Proof Explorer

Theorem iinfssclem1

Description: Lemma for iinfssc . (Contributed by Zhi Wang, 31-Oct-2025)

Ref Expression
Hypotheses iinfssc.1 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
iinfssc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat 𝐽 )
iinfssc.3 ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
iinfssclem1.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 = dom dom 𝐻 )
iinfssclem1.5 ⊢ Ⅎ 𝑥 𝜑
Assertion iinfssclem1 ( 𝜑 → 𝐾 = ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 , 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 iinfssc.1 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2 iinfssc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat 𝐽 )
3 iinfssc.3 ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
4 iinfssclem1.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 = dom dom 𝐻 )
5 iinfssclem1.5 ⊢ Ⅎ 𝑥 𝜑
6 2 4 sscfn1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn ( 𝑆 × 𝑆 ) )
7 6 fndmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom 𝐻 = ( 𝑆 × 𝑆 ) )
8 5 7 iineq2d ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 dom 𝐻 = ∩ 𝑥 ∈ 𝐴 ( 𝑆 × 𝑆 ) )
9 iinxp ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝑆 × 𝑆 ) = ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) )
10 1 9 syl ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 ( 𝑆 × 𝑆 ) = ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) )
11 8 10 eqtrd ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 dom 𝐻 = ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) )
12 11 mpteq1d ⊢ ( 𝜑 → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
13 3 12 eqtrd ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
14 fveq2 ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
15 df-ov ⊢ ( 𝑧 𝐻 𝑤 ) = ( 𝐻 ‘ ⟨ 𝑧 , 𝑤 ⟩ )
16 14 15 eqtr4di ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐻 ‘ 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
17 16 adantr ⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
18 17 iineq2dv ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) )
19 18 mpompt ⊢ ( 𝑦 ∈ ( ∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆 ) ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) = ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 , 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) )
20 13 19 eqtrdi ⊢ ( 𝜑 → 𝐾 = ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 , 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ) )