Metamath Proof Explorer

Theorem isopolem

Description: Lemma for isopo . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion isopolem ⊢HIsomR,SAB→SPoB→RPoA

Proof

Step Hyp Ref Expression
1 isof1o ⊢HIsomR,SAB→H:A⟶1-1 ontoB
2 f1of ⊢H:A⟶1-1 ontoB→H:A⟶B
3 ffvelcdm ⊢H:A⟶B∧d∈A→H⁡d∈B
4 3 ex ⊢H:A⟶B→d∈A→H⁡d∈B
5 ffvelcdm ⊢H:A⟶B∧e∈A→H⁡e∈B
6 5 ex ⊢H:A⟶B→e∈A→H⁡e∈B
7 ffvelcdm ⊢H:A⟶B∧f∈A→H⁡f∈B
8 7 ex ⊢H:A⟶B→f∈A→H⁡f∈B
9 4 6 8 3anim123d ⊢H:A⟶B→d∈A∧e∈A∧f∈A→H⁡d∈B∧H⁡e∈B∧H⁡f∈B
10 1 2 9 3syl ⊢HIsomR,SAB→d∈A∧e∈A∧f∈A→H⁡d∈B∧H⁡e∈B∧H⁡f∈B
11 10 imp ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→H⁡d∈B∧H⁡e∈B∧H⁡f∈B
12 breq12 ⊢a=H⁡d∧a=H⁡d→aSa↔H⁡dSH⁡d
13 12 anidms ⊢a=H⁡d→aSa↔H⁡dSH⁡d
14 13 notbid ⊢a=H⁡d→¬aSa↔¬H⁡dSH⁡d
15 breq1 ⊢a=H⁡d→aSb↔H⁡dSb
16 15 anbi1d ⊢a=H⁡d→aSb∧bSc↔H⁡dSb∧bSc
17 breq1 ⊢a=H⁡d→aSc↔H⁡dSc
18 16 17 imbi12d ⊢a=H⁡d→aSb∧bSc→aSc↔H⁡dSb∧bSc→H⁡dSc
19 14 18 anbi12d ⊢a=H⁡d→¬aSa∧aSb∧bSc→aSc↔¬H⁡dSH⁡d∧H⁡dSb∧bSc→H⁡dSc
20 breq2 ⊢b=H⁡e→H⁡dSb↔H⁡dSH⁡e
21 breq1 ⊢b=H⁡e→bSc↔H⁡eSc
22 20 21 anbi12d ⊢b=H⁡e→H⁡dSb∧bSc↔H⁡dSH⁡e∧H⁡eSc
23 22 imbi1d ⊢b=H⁡e→H⁡dSb∧bSc→H⁡dSc↔H⁡dSH⁡e∧H⁡eSc→H⁡dSc
24 23 anbi2d ⊢b=H⁡e→¬H⁡dSH⁡d∧H⁡dSb∧bSc→H⁡dSc↔¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSc→H⁡dSc
25 breq2 ⊢c=H⁡f→H⁡eSc↔H⁡eSH⁡f
26 25 anbi2d ⊢c=H⁡f→H⁡dSH⁡e∧H⁡eSc↔H⁡dSH⁡e∧H⁡eSH⁡f
27 breq2 ⊢c=H⁡f→H⁡dSc↔H⁡dSH⁡f
28 26 27 imbi12d ⊢c=H⁡f→H⁡dSH⁡e∧H⁡eSc→H⁡dSc↔H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
29 28 anbi2d ⊢c=H⁡f→¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSc→H⁡dSc↔¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
30 19 24 29 rspc3v ⊢H⁡d∈B∧H⁡e∈B∧H⁡f∈B→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
31 11 30 syl ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
32 simpl ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→HIsomR,SAB
33 simpr1 ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→d∈A
34 isorel ⊢HIsomR,SAB∧d∈A∧d∈A→dRd↔H⁡dSH⁡d
35 32 33 33 34 syl12anc ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→dRd↔H⁡dSH⁡d
36 35 notbid ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→¬dRd↔¬H⁡dSH⁡d
37 simpr2 ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→e∈A
38 isorel ⊢HIsomR,SAB∧d∈A∧e∈A→dRe↔H⁡dSH⁡e
39 32 33 37 38 syl12anc ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→dRe↔H⁡dSH⁡e
40 simpr3 ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→f∈A
41 isorel ⊢HIsomR,SAB∧e∈A∧f∈A→eRf↔H⁡eSH⁡f
42 32 37 40 41 syl12anc ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→eRf↔H⁡eSH⁡f
43 39 42 anbi12d ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→dRe∧eRf↔H⁡dSH⁡e∧H⁡eSH⁡f
44 isorel ⊢HIsomR,SAB∧d∈A∧f∈A→dRf↔H⁡dSH⁡f
45 32 33 40 44 syl12anc ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→dRf↔H⁡dSH⁡f
46 43 45 imbi12d ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→dRe∧eRf→dRf↔H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
47 36 46 anbi12d ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→¬dRd∧dRe∧eRf→dRf↔¬H⁡dSH⁡d∧H⁡dSH⁡e∧H⁡eSH⁡f→H⁡dSH⁡f
48 31 47 sylibrd ⊢HIsomR,SAB∧d∈A∧e∈A∧f∈A→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→¬dRd∧dRe∧eRf→dRf
49 48 ex ⊢HIsomR,SAB→d∈A∧e∈A∧f∈A→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→¬dRd∧dRe∧eRf→dRf
50 49 com23 ⊢HIsomR,SAB→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→d∈A∧e∈A∧f∈A→¬dRd∧dRe∧eRf→dRf
51 50 imp31 ⊢HIsomR,SAB∧∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc∧d∈A∧e∈A∧f∈A→¬dRd∧dRe∧eRf→dRf
52 51 ralrimivvva ⊢HIsomR,SAB∧∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→∀d∈A∀e∈A∀f∈A¬dRd∧dRe∧eRf→dRf
53 52 ex ⊢HIsomR,SAB→∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc→∀d∈A∀e∈A∀f∈A¬dRd∧dRe∧eRf→dRf
54 df-po ⊢SPoB↔∀a∈B∀b∈B∀c∈B¬aSa∧aSb∧bSc→aSc
55 df-po ⊢RPoA↔∀d∈A∀e∈A∀f∈A¬dRd∧dRe∧eRf→dRf
56 53 54 55 3imtr4g ⊢HIsomR,SAB→SPoB→RPoA