Theorem prtlem10

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

	Ref	Expression
Assertion	prtlem10	⊢ ( ∼ Er 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
2		simpl	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ∼ Er 𝐴 )
3	2 1	erref	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∼ 𝑧 )
4		breq1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∼ 𝑧 ↔ 𝑧 ∼ 𝑧 ) )
5		breq1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∼ 𝑤 ↔ 𝑧 ∼ 𝑤 ) )
6	4 5	anbi12d	⊢ ( 𝑣 = 𝑧 → ( ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ↔ ( 𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤 ) ) )
7	6	rspcev	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤 ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) )
8	7	expr	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∼ 𝑧 ) → ( 𝑧 ∼ 𝑤 → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) )
9	1 3 8	syl2anc	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∼ 𝑤 → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) )
10		simplll	⊢ ( ( ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) → ∼ Er 𝐴 )
11		simprl	⊢ ( ( ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑣 ∼ 𝑧 )
12		simprr	⊢ ( ( ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑣 ∼ 𝑤 )
13	10 11 12	ertr3d	⊢ ( ( ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑧 ∼ 𝑤 )
14	13	rexlimdva2	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) → 𝑧 ∼ 𝑤 ) )
15	9 14	impbid	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) ) )
16		vex	⊢ 𝑧 ∈ V
17		vex	⊢ 𝑣 ∈ V
18	16 17	elec	⊢ ( 𝑧 ∈ [ 𝑣 ] ∼ ↔ 𝑣 ∼ 𝑧 )
19		vex	⊢ 𝑤 ∈ V
20	19 17	elec	⊢ ( 𝑤 ∈ [ 𝑣 ] ∼ ↔ 𝑣 ∼ 𝑤 )
21	18 20	anbi12i	⊢ ( ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ↔ ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) )
22	21	rexbii	⊢ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤 ) )
23	15 22	bitr4di	⊢ ( ( ∼ Er 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ) )
24	23	ex	⊢ ( ∼ Er 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ) ) )