Metamath Proof Explorer

Theorem isoselem

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

Ref Expression
Hypotheses isofrlem.1 ⊢φ→HIsomR,SAB
isofrlem.2 ⊢φ→Hx∈V
Assertion isoselem ⊢φ→RSeA→SSeB

Proof

Step Hyp Ref Expression
1 isofrlem.1 ⊢φ→HIsomR,SAB
2 isofrlem.2 ⊢φ→Hx∈V
3 dfse2 ⊢RSeA↔∀z∈AA∩R-1z∈V
4 3 biimpi ⊢RSeA→∀z∈AA∩R-1z∈V
5 4 r19.21bi ⊢RSeA∧z∈A→A∩R-1z∈V
6 5 expcom ⊢z∈A→RSeA→A∩R-1z∈V
7 6 adantl ⊢φ∧z∈A→RSeA→A∩R-1z∈V
8 imaeq2 ⊢x=A∩R-1z→Hx=HA∩R-1z
9 8 eleq1d ⊢x=A∩R-1z→Hx∈V↔HA∩R-1z∈V
10 9 imbi2d ⊢x=A∩R-1z→φ→Hx∈V↔φ→HA∩R-1z∈V
11 10 2 vtoclg ⊢A∩R-1z∈V→φ→HA∩R-1z∈V
12 11 com12 ⊢φ→A∩R-1z∈V→HA∩R-1z∈V
13 12 adantr ⊢φ∧z∈A→A∩R-1z∈V→HA∩R-1z∈V
14 isoini ⊢HIsomR,SAB∧z∈A→HA∩R-1z=B∩S-1H⁡z
15 1 14 sylan ⊢φ∧z∈A→HA∩R-1z=B∩S-1H⁡z
16 15 eleq1d ⊢φ∧z∈A→HA∩R-1z∈V↔B∩S-1H⁡z∈V
17 13 16 sylibd ⊢φ∧z∈A→A∩R-1z∈V→B∩S-1H⁡z∈V
18 7 17 syld ⊢φ∧z∈A→RSeA→B∩S-1H⁡z∈V
19 18 ralrimdva ⊢φ→RSeA→∀z∈AB∩S-1H⁡z∈V
20 isof1o ⊢HIsomR,SAB→H:A⟶1-1 ontoB
21 f1ofn ⊢H:A⟶1-1 ontoB→HFnA
22 sneq ⊢y=H⁡z→y=H⁡z
23 22 imaeq2d ⊢y=H⁡z→S-1y=S-1H⁡z
24 23 ineq2d ⊢y=H⁡z→B∩S-1y=B∩S-1H⁡z
25 24 eleq1d ⊢y=H⁡z→B∩S-1y∈V↔B∩S-1H⁡z∈V
26 25 ralrn ⊢HFnA→∀y∈ran⁡HB∩S-1y∈V↔∀z∈AB∩S-1H⁡z∈V
27 1 20 21 26 4syl ⊢φ→∀y∈ran⁡HB∩S-1y∈V↔∀z∈AB∩S-1H⁡z∈V
28 f1ofo ⊢H:A⟶1-1 ontoB→H:A⟶ontoB
29 forn ⊢H:A⟶ontoB→ran⁡H=B
30 1 20 28 29 4syl ⊢φ→ran⁡H=B
31 30 raleqdv ⊢φ→∀y∈ran⁡HB∩S-1y∈V↔∀y∈BB∩S-1y∈V
32 27 31 bitr3d ⊢φ→∀z∈AB∩S-1H⁡z∈V↔∀y∈BB∩S-1y∈V
33 19 32 sylibd ⊢φ→RSeA→∀y∈BB∩S-1y∈V
34 dfse2 ⊢SSeB↔∀y∈BB∩S-1y∈V
35 33 34 imbitrrdi ⊢φ→RSeA→SSeB