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 A -> ( z e. A -> ( z .~ w <-> E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( .~ Er A /\ z e. A ) -> z e. A )
2		simpl	|- ( ( .~ Er A /\ z e. A ) -> .~ Er A )
3	2 1	erref	|- ( ( .~ Er A /\ z e. A ) -> z .~ z )
4		breq1	|- ( v = z -> ( v .~ z <-> z .~ z ) )
5		breq1	|- ( v = z -> ( v .~ w <-> z .~ w ) )
6	4 5	anbi12d	|- ( v = z -> ( ( v .~ z /\ v .~ w ) <-> ( z .~ z /\ z .~ w ) ) )
7	6	rspcev	|- ( ( z e. A /\ ( z .~ z /\ z .~ w ) ) -> E. v e. A ( v .~ z /\ v .~ w ) )
8	7	expr	|- ( ( z e. A /\ z .~ z ) -> ( z .~ w -> E. v e. A ( v .~ z /\ v .~ w ) ) )
9	1 3 8	syl2anc	|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w -> E. v e. A ( v .~ z /\ v .~ w ) ) )
10		simplll	|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> .~ Er A )
11		simprl	|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> v .~ z )
12		simprr	|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> v .~ w )
13	10 11 12	ertr3d	|- ( ( ( ( .~ Er A /\ z e. A ) /\ v e. A ) /\ ( v .~ z /\ v .~ w ) ) -> z .~ w )
14	13	rexlimdva2	|- ( ( .~ Er A /\ z e. A ) -> ( E. v e. A ( v .~ z /\ v .~ w ) -> z .~ w ) )
15	9 14	impbid	|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w <-> E. v e. A ( v .~ z /\ v .~ w ) ) )
16		vex	|- z e. _V
17		vex	|- v e. _V
18	16 17	elec	|- ( z e. [ v ] .~ <-> v .~ z )
19		vex	|- w e. _V
20	19 17	elec	|- ( w e. [ v ] .~ <-> v .~ w )
21	18 20	anbi12i	|- ( ( z e. [ v ] .~ /\ w e. [ v ] .~ ) <-> ( v .~ z /\ v .~ w ) )
22	21	rexbii	|- ( E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) <-> E. v e. A ( v .~ z /\ v .~ w ) )
23	15 22	bitr4di	|- ( ( .~ Er A /\ z e. A ) -> ( z .~ w <-> E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) ) )
24	23	ex	|- ( .~ Er A -> ( z e. A -> ( z .~ w <-> E. v e. A ( z e. [ v ] .~ /\ w e. [ v ] .~ ) ) ) )