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