Metamath Proof Explorer

Theorem 2reu4lem

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

Ref Expression
Assertion 2reu4lem ⊢A≠∅∧B≠∅→∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w

Proof

Step Hyp Ref Expression
1 reu3 ⊢∃!x∈A∃y∈Bφ↔∃x∈A∃y∈Bφ∧∃z∈A∀x∈A∃y∈Bφ→x=z
2 reu3 ⊢∃!y∈B∃x∈Aφ↔∃y∈B∃x∈Aφ∧∃w∈B∀y∈B∃x∈Aφ→y=w
3 1 2 anbi12i ⊢∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃y∈B∃x∈Aφ∧∃w∈B∀y∈B∃x∈Aφ→y=w
4 3 a1i ⊢A≠∅∧B≠∅→∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃y∈B∃x∈Aφ∧∃w∈B∀y∈B∃x∈Aφ→y=w
5 an4 ⊢∃x∈A∃y∈Bφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃y∈B∃x∈Aφ∧∃w∈B∀y∈B∃x∈Aφ→y=w↔∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃w∈B∀y∈B∃x∈Aφ→y=w
6 5 a1i ⊢A≠∅∧B≠∅→∃x∈A∃y∈Bφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃y∈B∃x∈Aφ∧∃w∈B∀y∈B∃x∈Aφ→y=w↔∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃w∈B∀y∈B∃x∈Aφ→y=w
7 rexcom ⊢∃y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ
8 7 anbi2i ⊢∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃x∈A∃y∈Bφ
9 anidm ⊢∃x∈A∃y∈Bφ∧∃x∈A∃y∈Bφ↔∃x∈A∃y∈Bφ
10 8 9 bitri ⊢∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ
11 10 a1i ⊢A≠∅∧B≠∅→∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ
12 r19.26 ⊢∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀x∈A∀y∈Bφ→y=w
13 nfra1 ⊢Ⅎx∀x∈A∀y∈Bφ→y=w
14 13 r19.3rz ⊢A≠∅→∀x∈A∀y∈Bφ→y=w↔∀x∈A∀x∈A∀y∈Bφ→y=w
15 14 bicomd ⊢A≠∅→∀x∈A∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→y=w
16 15 adantr ⊢A≠∅∧B≠∅→∀x∈A∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→y=w
17 16 adantr ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→y=w
18 17 anbi2d ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧∀x∈A∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
19 jcab ⊢φ→x=z∧y=w↔φ→x=z∧φ→y=w
20 19 ralbii ⊢∀y∈Bφ→x=z∧y=w↔∀y∈Bφ→x=z∧φ→y=w
21 r19.26 ⊢∀y∈Bφ→x=z∧φ→y=w↔∀y∈Bφ→x=z∧∀y∈Bφ→y=w
22 20 21 bitri ⊢∀y∈Bφ→x=z∧y=w↔∀y∈Bφ→x=z∧∀y∈Bφ→y=w
23 22 ralbii ⊢∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∀y∈Bφ→x=z∧∀y∈Bφ→y=w
24 r19.26 ⊢∀x∈A∀y∈Bφ→x=z∧∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
25 23 24 bitri ⊢∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
26 25 a1i ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
27 18 26 bitr4d ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧∀x∈A∀x∈A∀y∈Bφ→y=w↔∀x∈A∀y∈Bφ→x=z∧y=w
28 12 27 bitr2id ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
29 r19.26 ⊢∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∀y∈B∀y∈Bφ→x=z∧∀y∈B∀x∈Aφ→y=w
30 nfra1 ⊢Ⅎy∀y∈Bφ→x=z
31 30 r19.3rz ⊢B≠∅→∀y∈Bφ→x=z↔∀y∈B∀y∈Bφ→x=z
32 31 ad2antlr ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀y∈Bφ→x=z↔∀y∈B∀y∈Bφ→x=z
33 32 bicomd ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀y∈B∀y∈Bφ→x=z↔∀y∈Bφ→x=z
34 ralcom ⊢∀y∈B∀x∈Aφ→y=w↔∀x∈A∀y∈Bφ→y=w
35 34 a1i ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀y∈B∀x∈Aφ→y=w↔∀x∈A∀y∈Bφ→y=w
36 33 35 anbi12d ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀y∈B∀y∈Bφ→x=z∧∀y∈B∀x∈Aφ→y=w↔∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
37 29 36 bitrid ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
38 37 ralbidv ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∀x∈A∀y∈Bφ→x=z∧∀x∈A∀y∈Bφ→y=w
39 28 38 bitr4d ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w
40 r19.23v ⊢∀y∈Bφ→x=z↔∃y∈Bφ→x=z
41 r19.23v ⊢∀x∈Aφ→y=w↔∃x∈Aφ→y=w
42 40 41 anbi12i ⊢∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∃y∈Bφ→x=z∧∃x∈Aφ→y=w
43 42 2ralbii ⊢∀x∈A∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∀x∈A∀y∈B∃y∈Bφ→x=z∧∃x∈Aφ→y=w
44 43 a1i ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈B∀y∈Bφ→x=z∧∀x∈Aφ→y=w↔∀x∈A∀y∈B∃y∈Bφ→x=z∧∃x∈Aφ→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 ⊢Ⅎy∃y∈Bφ
52 nfv ⊢Ⅎyx=z
53 51 52 nfim ⊢Ⅎy∃y∈Bφ→x=z
54 nfre1 ⊢Ⅎx∃x∈Aφ
55 nfv ⊢Ⅎxy=w
56 54 55 nfim ⊢Ⅎx∃x∈Aφ→y=w
57 53 56 raaan2 ⊢A=∅↔B=∅→∀x∈A∀y∈B∃y∈Bφ→x=z∧∃x∈Aφ→y=w↔∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w
58 50 57 syl ⊢A≠∅∧B≠∅→∀x∈A∀y∈B∃y∈Bφ→x=z∧∃x∈Aφ→y=w↔∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w
59 58 adantr ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈B∃y∈Bφ→x=z∧∃x∈Aφ→y=w↔∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w
60 39 44 59 3bitrd ⊢A≠∅∧B≠∅∧z∈A∧w∈B→∀x∈A∀y∈Bφ→x=z∧y=w↔∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w
61 60 2rexbidva ⊢A≠∅∧B≠∅→∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w↔∃z∈A∃w∈B∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w
62 reeanv ⊢∃z∈A∃w∈B∀x∈A∃y∈Bφ→x=z∧∀y∈B∃x∈Aφ→y=w↔∃z∈A∀x∈A∃y∈Bφ→x=z∧∃w∈B∀y∈B∃x∈Aφ→y=w
63 61 62 bitr2di ⊢A≠∅∧B≠∅→∃z∈A∀x∈A∃y∈Bφ→x=z∧∃w∈B∀y∈B∃x∈Aφ→y=w↔∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w
64 11 63 anbi12d ⊢A≠∅∧B≠∅→∃x∈A∃y∈Bφ∧∃y∈B∃x∈Aφ∧∃z∈A∀x∈A∃y∈Bφ→x=z∧∃w∈B∀y∈B∃x∈Aφ→y=w↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w
65 4 6 64 3bitrd ⊢A≠∅∧B≠∅→∃!x∈A∃y∈Bφ∧∃!y∈B∃x∈Aφ↔∃x∈A∃y∈Bφ∧∃z∈A∃w∈B∀x∈A∀y∈Bφ→x=z∧y=w