This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrrdi ⊢ ( 𝜑 → ( 𝑅 Se 𝐴 → 𝑆 Se 𝐵 ) )