Metamath Proof Explorer

Theorem unirep

Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011)

Ref Expression
Hypotheses unirep.1 
|- ( y = D -> ( ph <-> ps ) )
unirep.2 
|- ( y = D -> B = C )
unirep.3 
|- ( y = z -> ( ph <-> ch ) )
unirep.4 
|- ( y = z -> B = F )
unirep.5 
|- B e. _V
Assertion unirep 
|- ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> ( iota x E. y e. A ( ph /\ x = B ) ) = C )

Proof

Step Hyp Ref Expression
1 unirep.1 
 |-  ( y = D -> ( ph <-> ps ) )
2 unirep.2 
 |-  ( y = D -> B = C )
3 unirep.3 
 |-  ( y = z -> ( ph <-> ch ) )
4 unirep.4 
 |-  ( y = z -> B = F )
5 unirep.5 
 |-  B e. _V
6 eqidd 
 |-  ( ps -> C = C )
7 6 ancli 
 |-  ( ps -> ( ps /\ C = C ) )
8 2 eqeq2d 
 |-  ( y = D -> ( C = B <-> C = C ) )
9 1 8 anbi12d 
 |-  ( y = D -> ( ( ph /\ C = B ) <-> ( ps /\ C = C ) ) )
10 9 rspcev 
 |-  ( ( D e. A /\ ( ps /\ C = C ) ) -> E. y e. A ( ph /\ C = B ) )
11 7 10 sylan2 
 |-  ( ( D e. A /\ ps ) -> E. y e. A ( ph /\ C = B ) )
12 11 adantl 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> E. y e. A ( ph /\ C = B ) )
13 nfcvd 
 |-  ( D e. A -> F/_ y C )
14 13 2 csbiegf 
 |-  ( D e. A -> [_ D / y ]_ B = C )
15 5 csbex 
 |-  [_ D / y ]_ B e. _V
16 14 15 eqeltrrdi 
 |-  ( D e. A -> C e. _V )
17 16 ad2antrl 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> C e. _V )
18 eqeq1 
 |-  ( x = C -> ( x = B <-> C = B ) )
19 18 anbi2d 
 |-  ( x = C -> ( ( ph /\ x = B ) <-> ( ph /\ C = B ) ) )
20 19 rexbidv 
 |-  ( x = C -> ( E. y e. A ( ph /\ x = B ) <-> E. y e. A ( ph /\ C = B ) ) )
21 20 spcegv 
 |-  ( C e. _V -> ( E. y e. A ( ph /\ C = B ) -> E. x E. y e. A ( ph /\ x = B ) ) )
22 16 21 syl 
 |-  ( D e. A -> ( E. y e. A ( ph /\ C = B ) -> E. x E. y e. A ( ph /\ x = B ) ) )
23 22 adantr 
 |-  ( ( D e. A /\ ps ) -> ( E. y e. A ( ph /\ C = B ) -> E. x E. y e. A ( ph /\ x = B ) ) )
24 11 23 mpd 
 |-  ( ( D e. A /\ ps ) -> E. x E. y e. A ( ph /\ x = B ) )
25 24 adantl 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> E. x E. y e. A ( ph /\ x = B ) )
26 r19.29 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ E. y e. A ( ph /\ x = B ) ) -> E. y e. A ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( ph /\ x = B ) ) )
27 r19.29 
 |-  ( ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ E. z e. A ( ch /\ w = F ) ) -> E. z e. A ( ( ( ph /\ ch ) -> B = F ) /\ ( ch /\ w = F ) ) )
28 an4 
 |-  ( ( ( ph /\ x = B ) /\ ( ch /\ w = F ) ) <-> ( ( ph /\ ch ) /\ ( x = B /\ w = F ) ) )
29 pm3.35 
 |-  ( ( ( ph /\ ch ) /\ ( ( ph /\ ch ) -> B = F ) ) -> B = F )
30 eqeq12 
 |-  ( ( x = B /\ w = F ) -> ( x = w <-> B = F ) )
31 29 30 syl5ibrcom 
 |-  ( ( ( ph /\ ch ) /\ ( ( ph /\ ch ) -> B = F ) ) -> ( ( x = B /\ w = F ) -> x = w ) )
32 31 ancoms 
 |-  ( ( ( ( ph /\ ch ) -> B = F ) /\ ( ph /\ ch ) ) -> ( ( x = B /\ w = F ) -> x = w ) )
33 32 expimpd 
 |-  ( ( ( ph /\ ch ) -> B = F ) -> ( ( ( ph /\ ch ) /\ ( x = B /\ w = F ) ) -> x = w ) )
34 28 33 syl5bi 
 |-  ( ( ( ph /\ ch ) -> B = F ) -> ( ( ( ph /\ x = B ) /\ ( ch /\ w = F ) ) -> x = w ) )
35 34 ancomsd 
 |-  ( ( ( ph /\ ch ) -> B = F ) -> ( ( ( ch /\ w = F ) /\ ( ph /\ x = B ) ) -> x = w ) )
36 35 expdimp 
 |-  ( ( ( ( ph /\ ch ) -> B = F ) /\ ( ch /\ w = F ) ) -> ( ( ph /\ x = B ) -> x = w ) )
37 36 rexlimivw 
 |-  ( E. z e. A ( ( ( ph /\ ch ) -> B = F ) /\ ( ch /\ w = F ) ) -> ( ( ph /\ x = B ) -> x = w ) )
38 37 imp 
 |-  ( ( E. z e. A ( ( ( ph /\ ch ) -> B = F ) /\ ( ch /\ w = F ) ) /\ ( ph /\ x = B ) ) -> x = w )
39 27 38 sylan 
 |-  ( ( ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ E. z e. A ( ch /\ w = F ) ) /\ ( ph /\ x = B ) ) -> x = w )
40 39 an32s 
 |-  ( ( ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( ph /\ x = B ) ) /\ E. z e. A ( ch /\ w = F ) ) -> x = w )
41 40 ex 
 |-  ( ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( ph /\ x = B ) ) -> ( E. z e. A ( ch /\ w = F ) -> x = w ) )
42 41 rexlimivw 
 |-  ( E. y e. A ( A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( ph /\ x = B ) ) -> ( E. z e. A ( ch /\ w = F ) -> x = w ) )
43 26 42 syl 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ E. y e. A ( ph /\ x = B ) ) -> ( E. z e. A ( ch /\ w = F ) -> x = w ) )
44 43 expimpd 
 |-  ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) -> ( ( E. y e. A ( ph /\ x = B ) /\ E. z e. A ( ch /\ w = F ) ) -> x = w ) )
45 44 adantr 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> ( ( E. y e. A ( ph /\ x = B ) /\ E. z e. A ( ch /\ w = F ) ) -> x = w ) )
46 45 alrimivv 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> A. x A. w ( ( E. y e. A ( ph /\ x = B ) /\ E. z e. A ( ch /\ w = F ) ) -> x = w ) )
47 eqeq1 
 |-  ( x = w -> ( x = B <-> w = B ) )
48 47 anbi2d 
 |-  ( x = w -> ( ( ph /\ x = B ) <-> ( ph /\ w = B ) ) )
49 48 rexbidv 
 |-  ( x = w -> ( E. y e. A ( ph /\ x = B ) <-> E. y e. A ( ph /\ w = B ) ) )
50 4 eqeq2d 
 |-  ( y = z -> ( w = B <-> w = F ) )
51 3 50 anbi12d 
 |-  ( y = z -> ( ( ph /\ w = B ) <-> ( ch /\ w = F ) ) )
52 51 cbvrexvw 
 |-  ( E. y e. A ( ph /\ w = B ) <-> E. z e. A ( ch /\ w = F ) )
53 49 52 bitrdi 
 |-  ( x = w -> ( E. y e. A ( ph /\ x = B ) <-> E. z e. A ( ch /\ w = F ) ) )
54 53 eu4 
 |-  ( E! x E. y e. A ( ph /\ x = B ) <-> ( E. x E. y e. A ( ph /\ x = B ) /\ A. x A. w ( ( E. y e. A ( ph /\ x = B ) /\ E. z e. A ( ch /\ w = F ) ) -> x = w ) ) )
55 25 46 54 sylanbrc 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> E! x E. y e. A ( ph /\ x = B ) )
56 20 iota2 
 |-  ( ( C e. _V /\ E! x E. y e. A ( ph /\ x = B ) ) -> ( E. y e. A ( ph /\ C = B ) <-> ( iota x E. y e. A ( ph /\ x = B ) ) = C ) )
57 17 55 56 syl2anc 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> ( E. y e. A ( ph /\ C = B ) <-> ( iota x E. y e. A ( ph /\ x = B ) ) = C ) )
58 12 57 mpbid 
 |-  ( ( A. y e. A A. z e. A ( ( ph /\ ch ) -> B = F ) /\ ( D e. A /\ ps ) ) -> ( iota x E. y e. A ( ph /\ x = B ) ) = C )