Metamath Proof Explorer

Theorem dfac5lem5

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

Ref Expression
Hypotheses dfac5lem.1 ⊢ A = u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t
dfac5lem.2 ⊢ B = ⋃ A ∩ y
dfac5lem.3 ⊢ φ ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
Assertion dfac5lem5 ⊢ φ → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w

Proof

Step Hyp Ref Expression
1 dfac5lem.1 ⊢ A = u | u ≠ ∅ ∧ ∃ t ∈ h u = t × t
2 dfac5lem.2 ⊢ B = ⋃ A ∩ y
3 dfac5lem.3 ⊢ φ ↔ ∀ x ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x z ≠ w → z ∩ w = ∅ → ∃ y ∀ z ∈ x ∃! v v ∈ z ∩ y
4 1 2 3 dfac5lem4 ⊢ φ → ∃ y ∀ z ∈ A ∃! v v ∈ z ∩ y
5 simpr ⊢ w ≠ ∅ ∧ w ∈ h → w ∈ h
6 5 a1i ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ≠ ∅ ∧ w ∈ h → w ∈ h
7 ineq1 ⊢ z = w × w → z ∩ y = w × w ∩ y
8 7 eleq2d ⊢ z = w × w → v ∈ z ∩ y ↔ v ∈ w × w ∩ y
9 8 eubidv ⊢ z = w × w → ∃! v v ∈ z ∩ y ↔ ∃! v v ∈ w × w ∩ y
10 9 rspccv ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w × w ∈ A → ∃! v v ∈ w × w ∩ y
11 1 dfac5lem3 ⊢ w × w ∈ A ↔ w ≠ ∅ ∧ w ∈ h
12 dfac5lem1 ⊢ ∃! v v ∈ w × w ∩ y ↔ ∃! g g ∈ w ∧ w g ∈ y
13 10 11 12 3imtr3g ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ≠ ∅ ∧ w ∈ h → ∃! g g ∈ w ∧ w g ∈ y
14 6 13 jcad ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ≠ ∅ ∧ w ∈ h → w ∈ h ∧ ∃! g g ∈ w ∧ w g ∈ y
15 2 eleq2i ⊢ w g ∈ B ↔ w g ∈ ⋃ A ∩ y
16 elin ⊢ w g ∈ ⋃ A ∩ y ↔ w g ∈ ⋃ A ∧ w g ∈ y
17 1 dfac5lem2 ⊢ w g ∈ ⋃ A ↔ w ∈ h ∧ g ∈ w
18 17 anbi1i ⊢ w g ∈ ⋃ A ∧ w g ∈ y ↔ w ∈ h ∧ g ∈ w ∧ w g ∈ y
19 anass ⊢ w ∈ h ∧ g ∈ w ∧ w g ∈ y ↔ w ∈ h ∧ g ∈ w ∧ w g ∈ y
20 18 19 bitri ⊢ w g ∈ ⋃ A ∧ w g ∈ y ↔ w ∈ h ∧ g ∈ w ∧ w g ∈ y
21 15 16 20 3bitri ⊢ w g ∈ B ↔ w ∈ h ∧ g ∈ w ∧ w g ∈ y
22 21 eubii ⊢ ∃! g w g ∈ B ↔ ∃! g w ∈ h ∧ g ∈ w ∧ w g ∈ y
23 euanv ⊢ ∃! g w ∈ h ∧ g ∈ w ∧ w g ∈ y ↔ w ∈ h ∧ ∃! g g ∈ w ∧ w g ∈ y
24 22 23 bitr2i ⊢ w ∈ h ∧ ∃! g g ∈ w ∧ w g ∈ y ↔ ∃! g w g ∈ B
25 14 24 syl6ib ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ≠ ∅ ∧ w ∈ h → ∃! g w g ∈ B
26 euex ⊢ ∃! g w g ∈ B → ∃ g w g ∈ B
27 nfeu1 ⊢ Ⅎ g ∃! g w g ∈ B
28 nfv ⊢ Ⅎ g B ⁡ w ∈ w
29 27 28 nfim ⊢ Ⅎ g ∃! g w g ∈ B → B ⁡ w ∈ w
30 21 simprbi ⊢ w g ∈ B → g ∈ w ∧ w g ∈ y
31 30 simpld ⊢ w g ∈ B → g ∈ w
32 tz6.12 ⊢ w g ∈ B ∧ ∃! g w g ∈ B → B ⁡ w = g
33 32 eleq1d ⊢ w g ∈ B ∧ ∃! g w g ∈ B → B ⁡ w ∈ w ↔ g ∈ w
34 33 biimparc ⊢ g ∈ w ∧ w g ∈ B ∧ ∃! g w g ∈ B → B ⁡ w ∈ w
35 34 exp32 ⊢ g ∈ w → w g ∈ B → ∃! g w g ∈ B → B ⁡ w ∈ w
36 31 35 mpcom ⊢ w g ∈ B → ∃! g w g ∈ B → B ⁡ w ∈ w
37 29 36 exlimi ⊢ ∃ g w g ∈ B → ∃! g w g ∈ B → B ⁡ w ∈ w
38 26 37 mpcom ⊢ ∃! g w g ∈ B → B ⁡ w ∈ w
39 25 38 syl6 ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ≠ ∅ ∧ w ∈ h → B ⁡ w ∈ w
40 39 expcomd ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → w ∈ h → w ≠ ∅ → B ⁡ w ∈ w
41 40 ralrimiv ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → ∀ w ∈ h w ≠ ∅ → B ⁡ w ∈ w
42 vex ⊢ y ∈ V
43 42 inex2 ⊢ ⋃ A ∩ y ∈ V
44 2 43 eqeltri ⊢ B ∈ V
45 fveq1 ⊢ f = B → f ⁡ w = B ⁡ w
46 45 eleq1d ⊢ f = B → f ⁡ w ∈ w ↔ B ⁡ w ∈ w
47 46 imbi2d ⊢ f = B → w ≠ ∅ → f ⁡ w ∈ w ↔ w ≠ ∅ → B ⁡ w ∈ w
48 47 ralbidv ⊢ f = B → ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w ↔ ∀ w ∈ h w ≠ ∅ → B ⁡ w ∈ w
49 44 48 spcev ⊢ ∀ w ∈ h w ≠ ∅ → B ⁡ w ∈ w → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
50 41 49 syl ⊢ ∀ z ∈ A ∃! v v ∈ z ∩ y → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
51 50 exlimiv ⊢ ∃ y ∀ z ∈ A ∃! v v ∈ z ∩ y → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w
52 4 51 syl ⊢ φ → ∃ f ∀ w ∈ h w ≠ ∅ → f ⁡ w ∈ w