This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-2025) (Proof shortened by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses upciclem1.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) )
upciclem1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
upciclem1.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
Assertion upciclem1 ( 𝜑 → ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )

Proof

Step Hyp Ref Expression
1 upciclem1.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) )
2 upciclem1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 upciclem1.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
4 eqeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
5 4 reubidv ⊢ ( 𝑛 = 𝑁 → ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
6 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
7 6 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑍 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
8 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
9 6 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) = ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) )
10 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
11 10 fveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) )
12 eqidd ⊢ ( 𝑦 = 𝑌 → 𝑀 = 𝑀 )
13 9 11 12 oveq123d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
14 13 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
15 8 14 reueqbidv ⊢ ( 𝑦 = 𝑌 → ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
16 7 15 raleqbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
17 16 1 2 rspcdva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
18 5 17 3 rspcdva ⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
19 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) )
20 19 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
21 20 eqeq2d ⊢ ( 𝑘 = 𝑚 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
22 21 cbvreuvw ⊢ ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
23 fveq2 ⊢ ( 𝑚 = 𝑙 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) )
24 23 oveq1d ⊢ ( 𝑚 = 𝑙 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
25 24 eqeq2d ⊢ ( 𝑚 = 𝑙 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
26 25 cbvreuvw ⊢ ( ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
27 22 26 bitri ⊢ ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
28 18 27 sylib ⊢ ( 𝜑 → ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )