Metamath Proof Explorer

Theorem dfac5lem1

Description: Lemma for dfac5 . (Contributed by NM, 12-Apr-2004)

Ref Expression
Assertion dfac5lem1 ⊢ ∃! v v ∈ w × w ∩ y ↔ ∃! g g ∈ w ∧ w g ∈ y

Proof

Step Hyp Ref Expression
1 elin ⊢ v ∈ w × w ∩ y ↔ v ∈ w × w ∧ v ∈ y
2 elxp ⊢ v ∈ w × w ↔ ∃ t ∃ g v = t g ∧ t ∈ w ∧ g ∈ w
3 excom ⊢ ∃ t ∃ g v = t g ∧ t ∈ w ∧ g ∈ w ↔ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w
4 2 3 bitri ⊢ v ∈ w × w ↔ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w
5 4 anbi1i ⊢ v ∈ w × w ∧ v ∈ y ↔ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y
6 19.41vv ⊢ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y
7 an32 ⊢ v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ v = t g ∧ v ∈ y ∧ t ∈ w ∧ g ∈ w
8 eleq1 ⊢ v = t g → v ∈ y ↔ t g ∈ y
9 8 pm5.32i ⊢ v = t g ∧ v ∈ y ↔ v = t g ∧ t g ∈ y
10 velsn ⊢ t ∈ w ↔ t = w
11 10 anbi1i ⊢ t ∈ w ∧ g ∈ w ↔ t = w ∧ g ∈ w
12 9 11 anbi12i ⊢ v = t g ∧ v ∈ y ∧ t ∈ w ∧ g ∈ w ↔ v = t g ∧ t g ∈ y ∧ t = w ∧ g ∈ w
13 an4 ⊢ v = t g ∧ t g ∈ y ∧ t = w ∧ g ∈ w ↔ v = t g ∧ t = w ∧ t g ∈ y ∧ g ∈ w
14 ancom ⊢ v = t g ∧ t = w ↔ t = w ∧ v = t g
15 ancom ⊢ t g ∈ y ∧ g ∈ w ↔ g ∈ w ∧ t g ∈ y
16 14 15 anbi12i ⊢ v = t g ∧ t = w ∧ t g ∈ y ∧ g ∈ w ↔ t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y
17 anass ⊢ t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y ↔ t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y
18 13 16 17 3bitri ⊢ v = t g ∧ t g ∈ y ∧ t = w ∧ g ∈ w ↔ t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y
19 7 12 18 3bitri ⊢ v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y
20 19 exbii ⊢ ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ ∃ t t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y
21 opeq1 ⊢ t = w → t g = w g
22 21 eqeq2d ⊢ t = w → v = t g ↔ v = w g
23 21 eleq1d ⊢ t = w → t g ∈ y ↔ w g ∈ y
24 23 anbi2d ⊢ t = w → g ∈ w ∧ t g ∈ y ↔ g ∈ w ∧ w g ∈ y
25 22 24 anbi12d ⊢ t = w → v = t g ∧ g ∈ w ∧ t g ∈ y ↔ v = w g ∧ g ∈ w ∧ w g ∈ y
26 25 equsexvw ⊢ ∃ t t = w ∧ v = t g ∧ g ∈ w ∧ t g ∈ y ↔ v = w g ∧ g ∈ w ∧ w g ∈ y
27 20 26 bitri ⊢ ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ v = w g ∧ g ∈ w ∧ w g ∈ y
28 27 exbii ⊢ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ ∃ g v = w g ∧ g ∈ w ∧ w g ∈ y
29 6 28 bitr3i ⊢ ∃ g ∃ t v = t g ∧ t ∈ w ∧ g ∈ w ∧ v ∈ y ↔ ∃ g v = w g ∧ g ∈ w ∧ w g ∈ y
30 1 5 29 3bitri ⊢ v ∈ w × w ∩ y ↔ ∃ g v = w g ∧ g ∈ w ∧ w g ∈ y
31 30 eubii ⊢ ∃! v v ∈ w × w ∩ y ↔ ∃! v ∃ g v = w g ∧ g ∈ w ∧ w g ∈ y
32 vex ⊢ w ∈ V
33 32 euop2 ⊢ ∃! v ∃ g v = w g ∧ g ∈ w ∧ w g ∈ y ↔ ∃! g g ∈ w ∧ w g ∈ y
34 31 33 bitri ⊢ ∃! v v ∈ w × w ∩ y ↔ ∃! g g ∈ w ∧ w g ∈ y