Theorem isthincd2lem1

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

	Ref	Expression
Hypotheses	isthincd2lem1.1	|- ( ph -> X e. B )
	isthincd2lem1.2	|- ( ph -> Y e. B )
	isthincd2lem1.3	|- ( ph -> F e. ( X H Y ) )
	isthincd2lem1.4	|- ( ph -> G e. ( X H Y ) )
	isthincd2lem1.5	|- ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
Assertion	isthincd2lem1	|- ( ph -> F = G )

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem1.1	|- ( ph -> X e. B )
2		isthincd2lem1.2	|- ( ph -> Y e. B )
3		isthincd2lem1.3	|- ( ph -> F e. ( X H Y ) )
4		isthincd2lem1.4	|- ( ph -> G e. ( X H Y ) )
5		isthincd2lem1.5	|- ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
6		oveq1	|- ( x = z -> ( x H y ) = ( z H y ) )
7	6	eleq2d	|- ( x = z -> ( f e. ( x H y ) <-> f e. ( z H y ) ) )
8	7	mobidv	|- ( x = z -> ( E* f f e. ( x H y ) <-> E* f f e. ( z H y ) ) )
9		oveq2	|- ( y = w -> ( z H y ) = ( z H w ) )
10	9	eleq2d	|- ( y = w -> ( f e. ( z H y ) <-> f e. ( z H w ) ) )
11	10	mobidv	|- ( y = w -> ( E* f f e. ( z H y ) <-> E* f f e. ( z H w ) ) )
12	8 11	cbvral2vw	|- ( A. x e. B A. y e. B E* f f e. ( x H y ) <-> A. z e. B A. w e. B E* f f e. ( z H w ) )
13	5 12	sylib	|- ( ph -> A. z e. B A. w e. B E* f f e. ( z H w ) )
14		oveq1	|- ( z = X -> ( z H w ) = ( X H w ) )
15	14	eleq2d	|- ( z = X -> ( f e. ( z H w ) <-> f e. ( X H w ) ) )
16	15	mobidv	|- ( z = X -> ( E* f f e. ( z H w ) <-> E* f f e. ( X H w ) ) )
17		nfv	|- F/ k f e. ( X H w )
18		nfv	|- F/ f k e. ( X H w )
19		eleq1w	|- ( f = k -> ( f e. ( X H w ) <-> k e. ( X H w ) ) )
20	17 18 19	cbvmow	|- ( E* f f e. ( X H w ) <-> E* k k e. ( X H w ) )
21		oveq2	|- ( w = Y -> ( X H w ) = ( X H Y ) )
22	21	eleq2d	|- ( w = Y -> ( k e. ( X H w ) <-> k e. ( X H Y ) ) )
23	22	mobidv	|- ( w = Y -> ( E* k k e. ( X H w ) <-> E* k k e. ( X H Y ) ) )
24	20 23	bitrid	|- ( w = Y -> ( E* f f e. ( X H w ) <-> E* k k e. ( X H Y ) ) )
25		eqidd	|- ( ( ph /\ z = X ) -> B = B )
26	16 24 1 25 2	rspc2vd	|- ( ph -> ( A. z e. B A. w e. B E* f f e. ( z H w ) -> E* k k e. ( X H Y ) ) )
27	13 26	mpd	|- ( ph -> E* k k e. ( X H Y ) )
28		moel	|- ( E* k k e. ( X H Y ) <-> A. k e. ( X H Y ) A. l e. ( X H Y ) k = l )
29	27 28	sylib	|- ( ph -> A. k e. ( X H Y ) A. l e. ( X H Y ) k = l )
30		eqeq1	|- ( k = F -> ( k = l <-> F = l ) )
31		eqeq2	|- ( l = G -> ( F = l <-> F = G ) )
32		eqidd	|- ( ( ph /\ k = F ) -> ( X H Y ) = ( X H Y ) )
33	30 31 3 32 4	rspc2vd	|- ( ph -> ( A. k e. ( X H Y ) A. l e. ( X H Y ) k = l -> F = G ) )
34	29 33	mpd	|- ( ph -> F = G )