Metamath Proof Explorer

Theorem 2reu4lem

Description: Lemma for 2reu4 . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2reu4lem 
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )

Proof

Step Hyp Ref Expression
1 reu3 
 |-  ( E! x e. A E. y e. B ph <-> ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) )
2 reu3 
 |-  ( E! y e. B E. x e. A ph <-> ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) )
3 1 2 anbi12i 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) )
4 3 a1i 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) )
5 an4 
 |-  ( ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) )
6 5 a1i 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( ( E. x e. A E. y e. B ph /\ E. z e. A A. x e. A ( E. y e. B ph -> x = z ) ) /\ ( E. y e. B E. x e. A ph /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) ) )
7 rexcom 
 |-  ( E. y e. B E. x e. A ph <-> E. x e. A E. y e. B ph )
8 7 anbi2i 
 |-  ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. x e. A E. y e. B ph ) )
9 anidm 
 |-  ( ( E. x e. A E. y e. B ph /\ E. x e. A E. y e. B ph ) <-> E. x e. A E. y e. B ph )
10 8 9 bitri 
 |-  ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> E. x e. A E. y e. B ph )
11 10 a1i 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) <-> E. x e. A E. y e. B ph ) )
12 r19.26 
 |-  ( A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) )
13 nfra1 
 |-  F/ x A. x e. A A. y e. B ( ph -> y = w )
14 13 r19.3rz 
 |-  ( A =/= (/) -> ( A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) )
15 14 bicomd 
 |-  ( A =/= (/) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) )
16 15 adantr 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) )
17 16 adantr 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. x e. A A. y e. B ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) )
18 17 anbi2d 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
19 jcab 
 |-  ( ( ph -> ( x = z /\ y = w ) ) <-> ( ( ph -> x = z ) /\ ( ph -> y = w ) ) )
20 19 ralbii 
 |-  ( A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. y e. B ( ( ph -> x = z ) /\ ( ph -> y = w ) ) )
21 r19.26 
 |-  ( A. y e. B ( ( ph -> x = z ) /\ ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) )
22 20 21 bitri 
 |-  ( A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) )
23 22 ralbii 
 |-  ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) )
24 r19.26 
 |-  ( A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. y e. B ( ph -> y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) )
25 23 24 bitri 
 |-  ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) )
26 25 a1i 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
27 18 26 bitr4d 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. x e. A A. y e. B ( ph -> x = z ) /\ A. x e. A A. x e. A A. y e. B ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )
28 12 27 bitr2id 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
29 r19.26 
 |-  ( A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B A. y e. B ( ph -> x = z ) /\ A. y e. B A. x e. A ( ph -> y = w ) ) )
30 nfra1 
 |-  F/ y A. y e. B ( ph -> x = z )
31 30 r19.3rz 
 |-  ( B =/= (/) -> ( A. y e. B ( ph -> x = z ) <-> A. y e. B A. y e. B ( ph -> x = z ) ) )
32 31 ad2antlr 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B ( ph -> x = z ) <-> A. y e. B A. y e. B ( ph -> x = z ) ) )
33 32 bicomd 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B A. y e. B ( ph -> x = z ) <-> A. y e. B ( ph -> x = z ) ) )
34 ralcom 
 |-  ( A. y e. B A. x e. A ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) )
35 34 a1i 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B A. x e. A ( ph -> y = w ) <-> A. x e. A A. y e. B ( ph -> y = w ) ) )
36 33 35 anbi12d 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( ( A. y e. B A. y e. B ( ph -> x = z ) /\ A. y e. B A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
37 29 36 bitrid 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
38 37 ralbidv 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A ( A. y e. B ( ph -> x = z ) /\ A. x e. A A. y e. B ( ph -> y = w ) ) ) )
39 28 38 bitr4d 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) ) )
40 r19.23v 
 |-  ( A. y e. B ( ph -> x = z ) <-> ( E. y e. B ph -> x = z ) )
41 r19.23v 
 |-  ( A. x e. A ( ph -> y = w ) <-> ( E. x e. A ph -> y = w ) )
42 40 41 anbi12i 
 |-  ( ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) )
43 42 2ralbii 
 |-  ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) )
44 43 a1i 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( A. y e. B ( ph -> x = z ) /\ A. x e. A ( ph -> y = w ) ) <-> A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) ) )
45 neneq 
 |-  ( A =/= (/) -> -. A = (/) )
46 neneq 
 |-  ( B =/= (/) -> -. B = (/) )
47 45 46 anim12i 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( -. A = (/) /\ -. B = (/) ) )
48 47 olcd 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) )
49 dfbi3 
 |-  ( ( A = (/) <-> B = (/) ) <-> ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) )
50 48 49 sylibr 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( A = (/) <-> B = (/) ) )
51 nfre1 
 |-  F/ y E. y e. B ph
52 nfv 
 |-  F/ y x = z
53 51 52 nfim 
 |-  F/ y ( E. y e. B ph -> x = z )
54 nfre1 
 |-  F/ x E. x e. A ph
55 nfv 
 |-  F/ x y = w
56 54 55 nfim 
 |-  F/ x ( E. x e. A ph -> y = w )
57 53 56 raaan2 
 |-  ( ( A = (/) <-> B = (/) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) )
58 50 57 syl 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) )
59 58 adantr 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ( E. y e. B ph -> x = z ) /\ ( E. x e. A ph -> y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) )
60 39 44 59 3bitrd 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( z e. A /\ w e. B ) ) -> ( A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) )
61 60 2rexbidva 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> E. z e. A E. w e. B ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) ) )
62 reeanv 
 |-  ( E. z e. A E. w e. B ( A. x e. A ( E. y e. B ph -> x = z ) /\ A. y e. B ( E. x e. A ph -> y = w ) ) <-> ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) )
63 61 62 bitr2di 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) <-> E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )
64 11 63 anbi12d 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E. z e. A A. x e. A ( E. y e. B ph -> x = z ) /\ E. w e. B A. y e. B ( E. x e. A ph -> y = w ) ) ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )
65 4 6 64 3bitrd 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )