Metamath Proof Explorer

Theorem upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-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 6 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) = ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) )
9 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
10 9 fveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) )
11 eqidd ⊢ ( 𝑦 = 𝑌 → 𝑀 = 𝑀 )
12 8 10 11 oveq123d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
13 12 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
14 13 reubidv ⊢ ( 𝑦 = 𝑌 → ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
16 15 reueqdv ⊢ ( 𝑦 = 𝑌 → ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
17 14 16 bitrd ⊢ ( 𝑦 = 𝑌 → ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
18 7 17 raleqbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑦 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
19 18 1 2 rspcdva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑛 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
20 5 19 3 rspcdva ⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
21 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) )
22 21 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
23 22 eqeq2d ⊢ ( 𝑘 = 𝑚 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
24 23 cbvreuvw ⊢ ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
25 fveq2 ⊢ ( 𝑚 = 𝑙 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) )
26 25 oveq1d ⊢ ( 𝑚 = 𝑙 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
27 26 eqeq2d ⊢ ( 𝑚 = 𝑙 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
28 27 cbvreuvw ⊢ ( ∃! 𝑚 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑚 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
29 24 28 bitri ⊢ ( ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
30 20 29 sylib ⊢ ( 𝜑 → ∃! 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )