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

Metamath Proof Explorer

Theorem isthincd2lem1

Description: Lemma for isthincd2 and thincmo2 . (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isthincd2lem1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
isthincd2lem1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
isthincd2lem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
isthincd2lem1.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
Assertion isthincd2lem1 ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 isthincd2lem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2 isthincd2lem1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 isthincd2lem1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4 isthincd2lem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
5 isthincd2lem1.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
6 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑦 ) )
7 6 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑧 𝐻 𝑦 ) ) )
8 7 mobidv ⊢ ( 𝑥 = 𝑧 → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑦 ) ) )
9 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
10 9 eleq2d ⊢ ( 𝑦 = 𝑤 → ( 𝑓 ∈ ( 𝑧 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) ) )
11 10 mobidv ⊢ ( 𝑦 = 𝑤 → ( ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) ) )
12 8 11 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) )
13 5 12 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) )
14 oveq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 𝐻 𝑤 ) = ( 𝑋 𝐻 𝑤 ) )
15 14 eleq2d ⊢ ( 𝑧 = 𝑋 → ( 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) ↔ 𝑓 ∈ ( 𝑋 𝐻 𝑤 ) ) )
16 15 mobidv ⊢ ( 𝑧 = 𝑋 → ( ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑤 ) ) )
17 nfv ⊢ Ⅎ 𝑘 𝑓 ∈ ( 𝑋 𝐻 𝑤 )
18 nfv ⊢ Ⅎ 𝑓 𝑘 ∈ ( 𝑋 𝐻 𝑤 )
19 eleq1w ⊢ ( 𝑓 = 𝑘 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑤 ) ↔ 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) ) )
20 17 18 19 cbvmow ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑤 ) ↔ ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) )
21 oveq2 ⊢ ( 𝑤 = 𝑌 → ( 𝑋 𝐻 𝑤 ) = ( 𝑋 𝐻 𝑌 ) )
22 21 eleq2d ⊢ ( 𝑤 = 𝑌 → ( 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) ↔ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ) )
23 22 mobidv ⊢ ( 𝑤 = 𝑌 → ( ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) ↔ ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ) )
24 20 23 bitrid ⊢ ( 𝑤 = 𝑌 → ( ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑤 ) ↔ ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ) )
25 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 = 𝑋 ) → 𝐵 = 𝐵 )
26 16 24 1 25 2 rspc2vd ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑧 𝐻 𝑤 ) → ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ) )
27 13 26 mpd ⊢ ( 𝜑 → ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) )
28 moel ⊢ ( ∃* 𝑘 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ↔ ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑘 = 𝑙 )
29 27 28 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑘 = 𝑙 )
30 eqeq1 ⊢ ( 𝑘 = 𝐹 → ( 𝑘 = 𝑙 ↔ 𝐹 = 𝑙 ) )
31 eqeq2 ⊢ ( 𝑙 = 𝐺 → ( 𝐹 = 𝑙 ↔ 𝐹 = 𝐺 ) )
32 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐹 ) → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
33 30 31 3 32 4 rspc2vd ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑋 𝐻 𝑌 ) ∀ 𝑙 ∈ ( 𝑋 𝐻 𝑌 ) 𝑘 = 𝑙 → 𝐹 = 𝐺 ) )
34 29 33 mpd ⊢ ( 𝜑 → 𝐹 = 𝐺 )