Theorem tz6.26OLD

Description: Obsolete proof of tz6.26 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	tz6.26OLD	|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		wereu2	|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! y e. B A. x e. B -. x R y )
2		reurex	|- ( E! y e. B A. x e. B -. x R y -> E. y e. B A. x e. B -. x R y )
3	1 2	syl	|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B A. x e. B -. x R y )
4		rabeq0	|- ( { x e. B | x R y } = (/) <-> A. x e. B -. x R y )
5		dfrab3	|- { x e. B | x R y } = ( B i^i { x | x R y } )
6		vex	|- y e. _V
7	6	dfpred2	|- Pred ( R , B , y ) = ( B i^i { x | x R y } )
8	5 7	eqtr4i	|- { x e. B | x R y } = Pred ( R , B , y )
9	8	eqeq1i	|- ( { x e. B | x R y } = (/) <-> Pred ( R , B , y ) = (/) )
10	4 9	bitr3i	|- ( A. x e. B -. x R y <-> Pred ( R , B , y ) = (/) )
11	10	rexbii	|- ( E. y e. B A. x e. B -. x R y <-> E. y e. B Pred ( R , B , y ) = (/) )
12	3 11	sylib	|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )