Metamath Proof Explorer

Theorem prtlem16

Description: Lemma for prtex , prter2 and prter3 . (Contributed by Rodolfo Medina, 14-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem13.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
Assertion prtlem16 ⊢ dom ⁡ ∼ ˙ = ⋃ A

Proof

Step Hyp Ref Expression
1 prtlem13.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
2 vex ⊢ z ∈ V
3 2 eldm ⊢ z ∈ dom ⁡ ∼ ˙ ↔ ∃ w z ∼ ˙ w
4 1 prtlem13 ⊢ z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v
5 4 exbii ⊢ ∃ w z ∼ ˙ w ↔ ∃ w ∃ v ∈ A z ∈ v ∧ w ∈ v
6 elunii ⊢ z ∈ v ∧ v ∈ A → z ∈ ⋃ A
7 6 ancoms ⊢ v ∈ A ∧ z ∈ v → z ∈ ⋃ A
8 7 adantrr ⊢ v ∈ A ∧ z ∈ v ∧ w ∈ v → z ∈ ⋃ A
9 8 rexlimiva ⊢ ∃ v ∈ A z ∈ v ∧ w ∈ v → z ∈ ⋃ A
10 9 exlimiv ⊢ ∃ w ∃ v ∈ A z ∈ v ∧ w ∈ v → z ∈ ⋃ A
11 eluni2 ⊢ z ∈ ⋃ A ↔ ∃ v ∈ A z ∈ v
12 elequ1 ⊢ w = z → w ∈ v ↔ z ∈ v
13 12 anbi2d ⊢ w = z → z ∈ v ∧ w ∈ v ↔ z ∈ v ∧ z ∈ v
14 pm4.24 ⊢ z ∈ v ↔ z ∈ v ∧ z ∈ v
15 13 14 syl6bbr ⊢ w = z → z ∈ v ∧ w ∈ v ↔ z ∈ v
16 15 rexbidv ⊢ w = z → ∃ v ∈ A z ∈ v ∧ w ∈ v ↔ ∃ v ∈ A z ∈ v
17 2 16 spcev ⊢ ∃ v ∈ A z ∈ v → ∃ w ∃ v ∈ A z ∈ v ∧ w ∈ v
18 11 17 sylbi ⊢ z ∈ ⋃ A → ∃ w ∃ v ∈ A z ∈ v ∧ w ∈ v
19 10 18 impbii ⊢ ∃ w ∃ v ∈ A z ∈ v ∧ w ∈ v ↔ z ∈ ⋃ A
20 3 5 19 3bitri ⊢ z ∈ dom ⁡ ∼ ˙ ↔ z ∈ ⋃ A
21 20 eqriv ⊢ dom ⁡ ∼ ˙ = ⋃ A