Theorem isoselem

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

	Ref	Expression
Hypotheses	isofrlem.1	⊢ ( 𝜑 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
	isofrlem.2	⊢ ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V )
Assertion	isoselem	⊢ ( 𝜑 → ( 𝑅 Se 𝐴 → 𝑆 Se 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		isofrlem.1	⊢ ( 𝜑 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2		isofrlem.2	⊢ ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V )
3		dfse2	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V )
4	3	biimpi	⊢ ( 𝑅 Se 𝐴 → ∀ 𝑧 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V )
5	4	r19.21bi	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V )
6	5	expcom	⊢ ( 𝑧 ∈ 𝐴 → ( 𝑅 Se 𝐴 → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑅 Se 𝐴 → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V ) )
8		imaeq2	⊢ ( 𝑥 = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) → ( 𝐻 “ 𝑥 ) = ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) )
9	8	eleq1d	⊢ ( 𝑥 = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) → ( ( 𝐻 “ 𝑥 ) ∈ V ↔ ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ) )
10	9	imbi2d	⊢ ( 𝑥 = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) → ( ( 𝜑 → ( 𝐻 “ 𝑥 ) ∈ V ) ↔ ( 𝜑 → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ) ) )
11	10 2	vtoclg	⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V → ( 𝜑 → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ) )
12	11	com12	⊢ ( 𝜑 → ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ) )
14		isoini	⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) )
15	1 14	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) )
16	15	eleq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ) ∈ V ↔ ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
17	13 16	sylibd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑧 } ) ) ∈ V → ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
18	7 17	syld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑅 Se 𝐴 → ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
19	18	ralrimdva	⊢ ( 𝜑 → ( 𝑅 Se 𝐴 → ∀ 𝑧 ∈ 𝐴 ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
20		isof1o	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
21		f1ofn	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Fn 𝐴 )
22		sneq	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑧 ) → { 𝑦 } = { ( 𝐻 ‘ 𝑧 ) } )
23	22	imaeq2d	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑧 ) → ( ◡ 𝑆 “ { 𝑦 } ) = ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) )
24	23	ineq2d	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑧 ) → ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) )
25	24	eleq1d	⊢ ( 𝑦 = ( 𝐻 ‘ 𝑧 ) → ( ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ↔ ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
26	25	ralrn	⊢ ( 𝐻 Fn 𝐴 → ( ∀ 𝑦 ∈ ran 𝐻 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
27	1 20 21 26	4syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐻 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ) )
28		f1ofo	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –onto→ 𝐵 )
29		forn	⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → ran 𝐻 = 𝐵 )
30	1 20 28 29	4syl	⊢ ( 𝜑 → ran 𝐻 = 𝐵 )
31	30	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐻 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ) )
32	27 31	bitr3d	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑧 ) } ) ) ∈ V ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ) )
33	19 32	sylibd	⊢ ( 𝜑 → ( 𝑅 Se 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V ) )
34		dfse2	⊢ ( 𝑆 Se 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑦 } ) ) ∈ V )
35	33 34	syl6ibr	⊢ ( 𝜑 → ( 𝑅 Se 𝐴 → 𝑆 Se 𝐵 ) )