Metamath Proof Explorer

Theorem oppcup3lem

Description: Lemma for oppcup3 . (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

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