Metamath Proof Explorer

Theorem isores2

Description: An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion isores2 ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R},{S}\cap \left({B}×{B}\right)}\left({A},{B}\right)$

Proof

Step Hyp Ref Expression
1 f1of ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {H}:{A}⟶{B}$
2 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {x}\in {A}\right)\to {H}\left({x}\right)\in {B}$
3 2 adantrr ${⊢}\left({H}:{A}⟶{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to {H}\left({x}\right)\in {B}$
4 ffvelrn ${⊢}\left({H}:{A}⟶{B}\wedge {y}\in {A}\right)\to {H}\left({y}\right)\in {B}$
5 4 adantrl ${⊢}\left({H}:{A}⟶{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to {H}\left({y}\right)\in {B}$
6 brinxp ${⊢}\left({H}\left({x}\right)\in {B}\wedge {H}\left({y}\right)\in {B}\right)\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)$
7 3 5 6 syl2anc ${⊢}\left({H}:{A}⟶{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)$
8 1 7 sylan ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)$
9 8 anassrs ${⊢}\left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)$
10 9 bibi2d ${⊢}\left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left(\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\left({x}{R}{y}↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)\right)$
11 10 ralbidva ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge {x}\in {A}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)\right)$
12 11 ralbidva ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)\right)$
13 12 pm5.32i ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)\right)$
14 df-isom ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
15 df-isom ${⊢}{H}{Isom}_{{R},{S}\cap \left({B}×{B}\right)}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right)\left({S}\cap \left({B}×{B}\right)\right){H}\left({y}\right)\right)\right)$
16 13 14 15 3bitr4i ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R},{S}\cap \left({B}×{B}\right)}\left({A},{B}\right)$