# Metamath Proof Explorer

## Theorem isopolem

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

Ref Expression
Assertion isopolem ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left({S}\mathrm{Po}{B}\to {R}\mathrm{Po}{A}\right)$

### Proof

Step Hyp Ref Expression
1 isof1o ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{B}$
2 f1of ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {H}:{A}⟶{B}$
3 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {d}\in {A}\right)\to {H}\left({d}\right)\in {B}$
4 3 ex ${⊢}{H}:{A}⟶{B}\to \left({d}\in {A}\to {H}\left({d}\right)\in {B}\right)$
5 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {e}\in {A}\right)\to {H}\left({e}\right)\in {B}$
6 5 ex ${⊢}{H}:{A}⟶{B}\to \left({e}\in {A}\to {H}\left({e}\right)\in {B}\right)$
7 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {f}\in {A}\right)\to {H}\left({f}\right)\in {B}$
8 7 ex ${⊢}{H}:{A}⟶{B}\to \left({f}\in {A}\to {H}\left({f}\right)\in {B}\right)$
9 4 6 8 3anim123d ${⊢}{H}:{A}⟶{B}\to \left(\left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\to \left({H}\left({d}\right)\in {B}\wedge {H}\left({e}\right)\in {B}\wedge {H}\left({f}\right)\in {B}\right)\right)$
10 1 2 9 3syl ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left(\left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\to \left({H}\left({d}\right)\in {B}\wedge {H}\left({e}\right)\in {B}\wedge {H}\left({f}\right)\in {B}\right)\right)$
11 10 imp ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({H}\left({d}\right)\in {B}\wedge {H}\left({e}\right)\in {B}\wedge {H}\left({f}\right)\in {B}\right)$
12 breq12 ${⊢}\left({a}={H}\left({d}\right)\wedge {a}={H}\left({d}\right)\right)\to \left({a}{S}{a}↔{H}\left({d}\right){S}{H}\left({d}\right)\right)$
13 12 anidms ${⊢}{a}={H}\left({d}\right)\to \left({a}{S}{a}↔{H}\left({d}\right){S}{H}\left({d}\right)\right)$
14 13 notbid ${⊢}{a}={H}\left({d}\right)\to \left(¬{a}{S}{a}↔¬{H}\left({d}\right){S}{H}\left({d}\right)\right)$
15 breq1 ${⊢}{a}={H}\left({d}\right)\to \left({a}{S}{b}↔{H}\left({d}\right){S}{b}\right)$
16 15 anbi1d ${⊢}{a}={H}\left({d}\right)\to \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)↔\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)\right)$
17 breq1 ${⊢}{a}={H}\left({d}\right)\to \left({a}{S}{c}↔{H}\left({d}\right){S}{c}\right)$
18 16 17 imbi12d ${⊢}{a}={H}\left({d}\right)\to \left(\left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)↔\left(\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)$
19 14 18 anbi12d ${⊢}{a}={H}\left({d}\right)\to \left(\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)↔\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)\right)$
20 breq2 ${⊢}{b}={H}\left({e}\right)\to \left({H}\left({d}\right){S}{b}↔{H}\left({d}\right){S}{H}\left({e}\right)\right)$
21 breq1 ${⊢}{b}={H}\left({e}\right)\to \left({b}{S}{c}↔{H}\left({e}\right){S}{c}\right)$
22 20 21 anbi12d ${⊢}{b}={H}\left({e}\right)\to \left(\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)↔\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)\right)$
23 22 imbi1d ${⊢}{b}={H}\left({e}\right)\to \left(\left(\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)\to {H}\left({d}\right){S}{c}\right)↔\left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)$
24 23 anbi2d ${⊢}{b}={H}\left({e}\right)\to \left(\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{b}\wedge {b}{S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)↔\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)\right)$
25 breq2 ${⊢}{c}={H}\left({f}\right)\to \left({H}\left({e}\right){S}{c}↔{H}\left({e}\right){S}{H}\left({f}\right)\right)$
26 25 anbi2d ${⊢}{c}={H}\left({f}\right)\to \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)↔\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\right)$
27 breq2 ${⊢}{c}={H}\left({f}\right)\to \left({H}\left({d}\right){S}{c}↔{H}\left({d}\right){S}{H}\left({f}\right)\right)$
28 26 27 imbi12d ${⊢}{c}={H}\left({f}\right)\to \left(\left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)\to {H}\left({d}\right){S}{c}\right)↔\left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)$
29 28 anbi2d ${⊢}{c}={H}\left({f}\right)\to \left(\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{c}\right)\to {H}\left({d}\right){S}{c}\right)\right)↔\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)\right)$
30 19 24 29 rspc3v ${⊢}\left({H}\left({d}\right)\in {B}\wedge {H}\left({e}\right)\in {B}\wedge {H}\left({f}\right)\in {B}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)\right)$
31 11 30 syl ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)\right)$
32 simpl ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to {H}{Isom}_{{R},{S}}\left({A},{B}\right)$
33 simpr1 ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to {d}\in {A}$
34 isorel ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {d}\in {A}\right)\right)\to \left({d}{R}{d}↔{H}\left({d}\right){S}{H}\left({d}\right)\right)$
35 32 33 33 34 syl12anc ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({d}{R}{d}↔{H}\left({d}\right){S}{H}\left({d}\right)\right)$
36 35 notbid ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(¬{d}{R}{d}↔¬{H}\left({d}\right){S}{H}\left({d}\right)\right)$
37 simpr2 ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to {e}\in {A}$
38 isorel ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\right)\right)\to \left({d}{R}{e}↔{H}\left({d}\right){S}{H}\left({e}\right)\right)$
39 32 33 37 38 syl12anc ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({d}{R}{e}↔{H}\left({d}\right){S}{H}\left({e}\right)\right)$
40 simpr3 ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to {f}\in {A}$
41 isorel ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({e}{R}{f}↔{H}\left({e}\right){S}{H}\left({f}\right)\right)$
42 32 37 40 41 syl12anc ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({e}{R}{f}↔{H}\left({e}\right){S}{H}\left({f}\right)\right)$
43 39 42 anbi12d ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)↔\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\right)$
44 isorel ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {f}\in {A}\right)\right)\to \left({d}{R}{f}↔{H}\left({d}\right){S}{H}\left({f}\right)\right)$
45 32 33 40 44 syl12anc ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left({d}{R}{f}↔{H}\left({d}\right){S}{H}\left({f}\right)\right)$
46 43 45 imbi12d ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(\left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)↔\left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)$
47 36 46 anbi12d ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(\left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)↔\left(¬{H}\left({d}\right){S}{H}\left({d}\right)\wedge \left(\left({H}\left({d}\right){S}{H}\left({e}\right)\wedge {H}\left({e}\right){S}{H}\left({f}\right)\right)\to {H}\left({d}\right){S}{H}\left({f}\right)\right)\right)\right)$
48 31 47 sylibrd ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)\right)$
49 48 ex ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left(\left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)\right)\right)$
50 49 com23 ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \left(\left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\to \left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)\right)\right)$
51 50 imp31 ${⊢}\left(\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\right)\wedge \left({d}\in {A}\wedge {e}\in {A}\wedge {f}\in {A}\right)\right)\to \left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)$
52 51 ralrimivvva ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\right)\to \forall {d}\in {A}\phantom{\rule{.4em}{0ex}}\forall {e}\in {A}\phantom{\rule{.4em}{0ex}}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)$
53 52 ex ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)\to \forall {d}\in {A}\phantom{\rule{.4em}{0ex}}\forall {e}\in {A}\phantom{\rule{.4em}{0ex}}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)\right)$
54 df-po ${⊢}{S}\mathrm{Po}{B}↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}\forall {c}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{a}{S}{a}\wedge \left(\left({a}{S}{b}\wedge {b}{S}{c}\right)\to {a}{S}{c}\right)\right)$
55 df-po ${⊢}{R}\mathrm{Po}{A}↔\forall {d}\in {A}\phantom{\rule{.4em}{0ex}}\forall {e}\in {A}\phantom{\rule{.4em}{0ex}}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{d}{R}{d}\wedge \left(\left({d}{R}{e}\wedge {e}{R}{f}\right)\to {d}{R}{f}\right)\right)$
56 53 54 55 3imtr4g ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left({S}\mathrm{Po}{B}\to {R}\mathrm{Po}{A}\right)$