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 ∼ = ∪ 𝐴