Metamath Proof Explorer

Theorem prtlem15

Description: Lemma for prter1 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion prtlem15 ⊢ Prt A → ∃ x ∈ A ∃ y ∈ A u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → ∃ z ∈ A u ∈ z ∧ v ∈ z

Proof

Step Hyp Ref Expression
1 anabs7 ⊢ w ∈ x ∧ w ∈ y ∧ u ∈ x ∧ v ∈ y ∧ w ∈ x ∧ w ∈ y ↔ u ∈ x ∧ v ∈ y ∧ w ∈ x ∧ w ∈ y
2 an43 ⊢ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y ↔ u ∈ x ∧ v ∈ y ∧ w ∈ x ∧ w ∈ y
3 2 anbi2i ⊢ w ∈ x ∧ w ∈ y ∧ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y ↔ w ∈ x ∧ w ∈ y ∧ u ∈ x ∧ v ∈ y ∧ w ∈ x ∧ w ∈ y
4 1 3 2 3bitr4ri ⊢ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y ↔ w ∈ x ∧ w ∈ y ∧ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y
5 prtlem14 ⊢ Prt A → x ∈ A ∧ y ∈ A → w ∈ x ∧ w ∈ y → x = y
6 an3 ⊢ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ y
7 elequ2 ⊢ x = y → v ∈ x ↔ v ∈ y
8 7 anbi2d ⊢ x = y → u ∈ x ∧ v ∈ x ↔ u ∈ x ∧ v ∈ y
9 6 8 syl5ibr ⊢ x = y → u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
10 5 9 syl8 ⊢ Prt A → x ∈ A ∧ y ∈ A → w ∈ x ∧ w ∈ y → u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
11 10 imp4a ⊢ Prt A → x ∈ A ∧ y ∈ A → w ∈ x ∧ w ∈ y ∧ u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
12 4 11 syl7bi ⊢ Prt A → x ∈ A ∧ y ∈ A → u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
13 12 expdimp ⊢ Prt A ∧ x ∈ A → y ∈ A → u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
14 13 rexlimdv ⊢ Prt A ∧ x ∈ A → ∃ y ∈ A u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → u ∈ x ∧ v ∈ x
15 14 reximdva ⊢ Prt A → ∃ x ∈ A ∃ y ∈ A u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → ∃ x ∈ A u ∈ x ∧ v ∈ x
16 elequ2 ⊢ x = z → u ∈ x ↔ u ∈ z
17 elequ2 ⊢ x = z → v ∈ x ↔ v ∈ z
18 16 17 anbi12d ⊢ x = z → u ∈ x ∧ v ∈ x ↔ u ∈ z ∧ v ∈ z
19 18 cbvrexvw ⊢ ∃ x ∈ A u ∈ x ∧ v ∈ x ↔ ∃ z ∈ A u ∈ z ∧ v ∈ z
20 15 19 syl6ib ⊢ Prt A → ∃ x ∈ A ∃ y ∈ A u ∈ x ∧ w ∈ x ∧ w ∈ y ∧ v ∈ y → ∃ z ∈ A u ∈ z ∧ v ∈ z