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 
|- ( 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 )