This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion prtlem16 dom ∼ = ∪ 𝐴

Proof

Step Hyp Ref Expression
1 prtlem13.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2 vex ⊢ 𝑧 ∈ V
3 2 eldm ⊢ ( 𝑧 ∈ dom ∼ ↔ ∃ 𝑤 𝑧 ∼ 𝑤 )
4 1 prtlem13 ⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
5 4 exbii ⊢ ( ∃ 𝑤 𝑧 ∼ 𝑤 ↔ ∃ 𝑤 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
6 elunii ⊢ ( ( 𝑧 ∈ 𝑣 ∧ 𝑣 ∈ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 )
7 6 ancoms ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ ∪ 𝐴 )
8 7 adantrr ⊢ ( ( 𝑣 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑧 ∈ ∪ 𝐴 )
9 8 rexlimiva ⊢ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑧 ∈ ∪ 𝐴 )
10 9 exlimiv ⊢ ( ∃ 𝑤 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑧 ∈ ∪ 𝐴 )
11 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 )
12 elequ1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∈ 𝑣 ) )
13 12 anbi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) ) )
14 pm4.24 ⊢ ( 𝑧 ∈ 𝑣 ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) )
15 13 14 bitr4di ⊢ ( 𝑤 = 𝑧 → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ 𝑧 ∈ 𝑣 ) )
16 15 rexbidv ⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ) )
17 2 16 spcev ⊢ ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 → ∃ 𝑤 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
18 11 17 sylbi ⊢ ( 𝑧 ∈ ∪ 𝐴 → ∃ 𝑤 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
19 10 18 impbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ 𝑧 ∈ ∪ 𝐴 )
20 3 5 19 3bitri ⊢ ( 𝑧 ∈ dom ∼ ↔ 𝑧 ∈ ∪ 𝐴 )
21 20 eqriv ⊢ dom ∼ = ∪ 𝐴