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	⊢ ( 𝜑 → 𝐹 = 𝐺 )