Metamath Proof Explorer

Theorem br4

Description: Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013) (Revised by Mario Carneiro, 14-Oct-2013)

Ref Expression
Hypotheses br4.1 
|- ( a = A -> ( ph <-> ps ) )
br4.2 
|- ( b = B -> ( ps <-> ch ) )
br4.3 
|- ( c = C -> ( ch <-> th ) )
br4.4 
|- ( d = D -> ( th <-> ta ) )
br4.5 
|- ( x = X -> P = Q )
br4.6 
|- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) }
Assertion br4 
|- ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( <. A , B >. R <. C , D >. <-> ta ) )

Proof

Step Hyp Ref Expression
1 br4.1 
 |-  ( a = A -> ( ph <-> ps ) )
2 br4.2 
 |-  ( b = B -> ( ps <-> ch ) )
3 br4.3 
 |-  ( c = C -> ( ch <-> th ) )
4 br4.4 
 |-  ( d = D -> ( th <-> ta ) )
5 br4.5 
 |-  ( x = X -> P = Q )
6 br4.6 
 |-  R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) }
7 opex 
 |-  <. A , B >. e. _V
8 opex 
 |-  <. C , D >. e. _V
9 eqeq1 
 |-  ( p = <. A , B >. -> ( p = <. a , b >. <-> <. A , B >. = <. a , b >. ) )
10 9 3anbi1d 
 |-  ( p = <. A , B >. -> ( ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) ) )
11 10 rexbidv 
 |-  ( p = <. A , B >. -> ( E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) ) )
12 11 2rexbidv 
 |-  ( p = <. A , B >. -> ( E. b e. P E. c e. P E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) ) )
13 12 2rexbidv 
 |-  ( p = <. A , B >. -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( p = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) ) )
14 eqeq1 
 |-  ( q = <. C , D >. -> ( q = <. c , d >. <-> <. C , D >. = <. c , d >. ) )
15 14 3anbi2d 
 |-  ( q = <. C , D >. -> ( ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
16 15 rexbidv 
 |-  ( q = <. C , D >. -> ( E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
17 16 2rexbidv 
 |-  ( q = <. C , D >. -> ( E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
18 17 2rexbidv 
 |-  ( q = <. C , D >. -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ q = <. c , d >. /\ ph ) <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
19 7 8 13 18 6 brab 
 |-  ( <. A , B >. R <. C , D >. <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) )
20 vex 
 |-  a e. _V
21 vex 
 |-  b e. _V
22 20 21 opth 
 |-  ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
23 1 2 sylan9bb 
 |-  ( ( a = A /\ b = B ) -> ( ph <-> ch ) )
24 22 23 sylbi 
 |-  ( <. a , b >. = <. A , B >. -> ( ph <-> ch ) )
25 24 eqcoms 
 |-  ( <. A , B >. = <. a , b >. -> ( ph <-> ch ) )
26 vex 
 |-  c e. _V
27 vex 
 |-  d e. _V
28 26 27 opth 
 |-  ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
29 3 4 sylan9bb 
 |-  ( ( c = C /\ d = D ) -> ( ch <-> ta ) )
30 28 29 sylbi 
 |-  ( <. c , d >. = <. C , D >. -> ( ch <-> ta ) )
31 30 eqcoms 
 |-  ( <. C , D >. = <. c , d >. -> ( ch <-> ta ) )
32 25 31 sylan9bb 
 |-  ( ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. ) -> ( ph <-> ta ) )
33 32 biimp3a 
 |-  ( ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) -> ta )
34 33 a1i 
 |-  ( ( ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ d e. P ) -> ( ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) -> ta ) )
35 34 rexlimdva 
 |-  ( ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) -> ( E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) -> ta ) )
36 35 rexlimdvva 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ( x e. S /\ a e. P ) ) -> ( E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) -> ta ) )
37 36 rexlimdvva 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) -> ta ) )
38 simpl1 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> X e. S )
39 simpl2l 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> A e. Q )
40 simpl2r 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> B e. Q )
41 simpl3l 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> C e. Q )
42 simpl3r 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> D e. Q )
43 eqidd 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> <. A , B >. = <. A , B >. )
44 eqidd 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> <. C , D >. = <. C , D >. )
45 simpr 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> ta )
46 opeq1 
 |-  ( c = C -> <. c , d >. = <. C , d >. )
47 46 eqeq2d 
 |-  ( c = C -> ( <. C , D >. = <. c , d >. <-> <. C , D >. = <. C , d >. ) )
48 47 3 3anbi23d 
 |-  ( c = C -> ( ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) <-> ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , d >. /\ th ) ) )
49 opeq2 
 |-  ( d = D -> <. C , d >. = <. C , D >. )
50 49 eqeq2d 
 |-  ( d = D -> ( <. C , D >. = <. C , d >. <-> <. C , D >. = <. C , D >. ) )
51 50 4 3anbi23d 
 |-  ( d = D -> ( ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , d >. /\ th ) <-> ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , D >. /\ ta ) ) )
52 48 51 rspc2ev 
 |-  ( ( C e. Q /\ D e. Q /\ ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , D >. /\ ta ) ) -> E. c e. Q E. d e. Q ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) )
53 41 42 43 44 45 52 syl113anc 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> E. c e. Q E. d e. Q ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) )
54 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
55 54 eqeq2d 
 |-  ( a = A -> ( <. A , B >. = <. a , b >. <-> <. A , B >. = <. A , b >. ) )
56 55 1 3anbi13d 
 |-  ( a = A -> ( ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> ( <. A , B >. = <. A , b >. /\ <. C , D >. = <. c , d >. /\ ps ) ) )
57 56 2rexbidv 
 |-  ( a = A -> ( E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> E. c e. Q E. d e. Q ( <. A , B >. = <. A , b >. /\ <. C , D >. = <. c , d >. /\ ps ) ) )
58 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
59 58 eqeq2d 
 |-  ( b = B -> ( <. A , B >. = <. A , b >. <-> <. A , B >. = <. A , B >. ) )
60 59 2 3anbi13d 
 |-  ( b = B -> ( ( <. A , B >. = <. A , b >. /\ <. C , D >. = <. c , d >. /\ ps ) <-> ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) ) )
61 60 2rexbidv 
 |-  ( b = B -> ( E. c e. Q E. d e. Q ( <. A , B >. = <. A , b >. /\ <. C , D >. = <. c , d >. /\ ps ) <-> E. c e. Q E. d e. Q ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) ) )
62 57 61 rspc2ev 
 |-  ( ( A e. Q /\ B e. Q /\ E. c e. Q E. d e. Q ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. c , d >. /\ ch ) ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) )
63 39 40 53 62 syl3anc 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) )
64 5 rexeqdv 
 |-  ( x = X -> ( E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
65 5 64 rexeqbidv 
 |-  ( x = X -> ( E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
66 5 65 rexeqbidv 
 |-  ( x = X -> ( E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> E. b e. Q E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
67 5 66 rexeqbidv 
 |-  ( x = X -> ( E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> E. a e. Q E. b e. Q E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
68 67 rspcev 
 |-  ( ( X e. S /\ E. a e. Q E. b e. Q E. c e. Q E. d e. Q ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) )
69 38 63 68 syl2anc 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) /\ ta ) -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) )
70 69 ex 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( ta -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) ) )
71 37 70 impbid 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P ( <. A , B >. = <. a , b >. /\ <. C , D >. = <. c , d >. /\ ph ) <-> ta ) )
72 19 71 bitrid 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q ) ) -> ( <. A , B >. R <. C , D >. <-> ta ) )