Theorem prtlem19

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

	Ref	Expression
Hypothesis	prtlem18.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion	prtlem19	⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → 𝑣 = [ 𝑧 ] ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2	1	prtlem18	⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤 ) ) )
3	2	imp	⊢ ( ( Prt 𝐴 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤 ) )
4		vex	⊢ 𝑤 ∈ V
5		vex	⊢ 𝑧 ∈ V
6	4 5	elec	⊢ ( 𝑤 ∈ [ 𝑧 ] ∼ ↔ 𝑧 ∼ 𝑤 )
7	3 6	bitr4di	⊢ ( ( Prt 𝐴 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ [ 𝑧 ] ∼ ) )
8	7	eqrdv	⊢ ( ( Prt 𝐴 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 = [ 𝑧 ] ∼ )
9	8	ex	⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → 𝑣 = [ 𝑧 ] ∼ ) )