Theorem isoselem

Description: Lemma for isose . (Contributed by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Hypotheses	isofrlem.1	|- ( ph -> H Isom R , S ( A , B ) )
	isofrlem.2	|- ( ph -> ( H " x ) e. _V )
Assertion	isoselem	|- ( ph -> ( R Se A -> S Se B ) )

Proof

Step	Hyp	Ref	Expression
1		isofrlem.1	|- ( ph -> H Isom R , S ( A , B ) )
2		isofrlem.2	|- ( ph -> ( H " x ) e. _V )
3		dfse2	|- ( R Se A <-> A. z e. A ( A i^i ( `' R " { z } ) ) e. _V )
4	3	biimpi	|- ( R Se A -> A. z e. A ( A i^i ( `' R " { z } ) ) e. _V )
5	4	r19.21bi	|- ( ( R Se A /\ z e. A ) -> ( A i^i ( `' R " { z } ) ) e. _V )
6	5	expcom	|- ( z e. A -> ( R Se A -> ( A i^i ( `' R " { z } ) ) e. _V ) )
7	6	adantl	|- ( ( ph /\ z e. A ) -> ( R Se A -> ( A i^i ( `' R " { z } ) ) e. _V ) )
8		imaeq2	|- ( x = ( A i^i ( `' R " { z } ) ) -> ( H " x ) = ( H " ( A i^i ( `' R " { z } ) ) ) )
9	8	eleq1d	|- ( x = ( A i^i ( `' R " { z } ) ) -> ( ( H " x ) e. _V <-> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
10	9	imbi2d	|- ( x = ( A i^i ( `' R " { z } ) ) -> ( ( ph -> ( H " x ) e. _V ) <-> ( ph -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) ) )
11	10 2	vtoclg	|- ( ( A i^i ( `' R " { z } ) ) e. _V -> ( ph -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
12	11	com12	|- ( ph -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
13	12	adantr	|- ( ( ph /\ z e. A ) -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
14		isoini	|- ( ( H Isom R , S ( A , B ) /\ z e. A ) -> ( H " ( A i^i ( `' R " { z } ) ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
15	1 14	sylan	|- ( ( ph /\ z e. A ) -> ( H " ( A i^i ( `' R " { z } ) ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
16	15	eleq1d	|- ( ( ph /\ z e. A ) -> ( ( H " ( A i^i ( `' R " { z } ) ) ) e. _V <-> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
17	13 16	sylibd	|- ( ( ph /\ z e. A ) -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
18	7 17	syld	|- ( ( ph /\ z e. A ) -> ( R Se A -> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
19	18	ralrimdva	|- ( ph -> ( R Se A -> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
20		isof1o	|- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
21		f1ofn	|- ( H : A -1-1-onto-> B -> H Fn A )
22		sneq	|- ( y = ( H ` z ) -> { y } = { ( H ` z ) } )
23	22	imaeq2d	|- ( y = ( H ` z ) -> ( `' S " { y } ) = ( `' S " { ( H ` z ) } ) )
24	23	ineq2d	|- ( y = ( H ` z ) -> ( B i^i ( `' S " { y } ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
25	24	eleq1d	|- ( y = ( H ` z ) -> ( ( B i^i ( `' S " { y } ) ) e. _V <-> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
26	25	ralrn	|- ( H Fn A -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
27	1 20 21 26	4syl	|- ( ph -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
28		f1ofo	|- ( H : A -1-1-onto-> B -> H : A -onto-> B )
29		forn	|- ( H : A -onto-> B -> ran H = B )
30	1 20 28 29	4syl	|- ( ph -> ran H = B )
31	30	raleqdv	|- ( ph -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
32	27 31	bitr3d	|- ( ph -> ( A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
33	19 32	sylibd	|- ( ph -> ( R Se A -> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
34		dfse2	|- ( S Se B <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V )
35	33 34	syl6ibr	|- ( ph -> ( R Se A -> S Se B ) )