f1oiso2

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . (Contributed by Mario Carneiro, 9-Mar-2013)

		Ref	Expression
	Hypothesis	f1oiso2.1	$⊢ S = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y))\}$
	Assertion	f1oiso2	$⊢ H : A \underset{1-1 onto}{⟶} B \to H {Isom}_{R, S} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		f1oiso2.1	$⊢ S = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y))\}$
2		f1ocnvdm	$⊢ (H : A \underset{1-1 onto}{⟶} B \land x \in B) \to H^{-1} (x) \in A$
3	2	adantrr	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B)) \to H^{-1} (x) \in A$
4	3	3adant3	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to H^{-1} (x) \in A$
5		f1ocnvdm	$⊢ (H : A \underset{1-1 onto}{⟶} B \land y \in B) \to H^{-1} (y) \in A$
6	5	adantrl	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B)) \to H^{-1} (y) \in A$
7	6	3adant3	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to H^{-1} (y) \in A$
8		f1ocnvfv2	$⊢ (H : A \underset{1-1 onto}{⟶} B \land x \in B) \to H (H^{-1} (x)) = x$
9	8	eqcomd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land x \in B) \to x = H (H^{-1} (x))$
10		f1ocnvfv2	$⊢ (H : A \underset{1-1 onto}{⟶} B \land y \in B) \to H (H^{-1} (y)) = y$
11	10	eqcomd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land y \in B) \to y = H (H^{-1} (y))$
12	9 11	anim12dan	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B)) \to (x = H (H^{-1} (x)) \land y = H (H^{-1} (y)))$
13	12	3adant3	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to (x = H (H^{-1} (x)) \land y = H (H^{-1} (y)))$
14		simp3	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to H^{-1} (x) R H^{-1} (y)$
15		fveq2	$⊢ w = H^{-1} (y) \to H (w) = H (H^{-1} (y))$
16	15	eqeq2d	$⊢ w = H^{-1} (y) \to (y = H (w) \leftrightarrow y = H (H^{-1} (y)))$
17	16	anbi2d	$⊢ w = H^{-1} (y) \to ((x = H (H^{-1} (x)) \land y = H (w)) \leftrightarrow (x = H (H^{-1} (x)) \land y = H (H^{-1} (y))))$
18		breq2	$⊢ w = H^{-1} (y) \to (H^{-1} (x) R w \leftrightarrow H^{-1} (x) R H^{-1} (y))$
19	17 18	anbi12d	$⊢ w = H^{-1} (y) \to (((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w) \leftrightarrow ((x = H (H^{-1} (x)) \land y = H (H^{-1} (y))) \land H^{-1} (x) R H^{-1} (y)))$
20	19	rspcev	$⊢ (H^{-1} (y) \in A \land ((x = H (H^{-1} (x)) \land y = H (H^{-1} (y))) \land H^{-1} (x) R H^{-1} (y))) \to \exists w \in A ((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w)$
21	7 13 14 20	syl12anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to \exists w \in A ((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w)$
22		fveq2	$⊢ z = H^{-1} (x) \to H (z) = H (H^{-1} (x))$
23	22	eqeq2d	$⊢ z = H^{-1} (x) \to (x = H (z) \leftrightarrow x = H (H^{-1} (x)))$
24	23	anbi1d	$⊢ z = H^{-1} (x) \to ((x = H (z) \land y = H (w)) \leftrightarrow (x = H (H^{-1} (x)) \land y = H (w)))$
25		breq1	$⊢ z = H^{-1} (x) \to (z R w \leftrightarrow H^{-1} (x) R w)$
26	24 25	anbi12d	$⊢ z = H^{-1} (x) \to (((x = H (z) \land y = H (w)) \land z R w) \leftrightarrow ((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w))$
27	26	rexbidv	$⊢ z = H^{-1} (x) \to (\exists w \in A ((x = H (z) \land y = H (w)) \land z R w) \leftrightarrow \exists w \in A ((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w))$
28	27	rspcev	$⊢ (H^{-1} (x) \in A \land \exists w \in A ((x = H (H^{-1} (x)) \land y = H (w)) \land H^{-1} (x) R w)) \to \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w)$
29	4 21 28	syl2anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w)$
30	29	3expib	$⊢ H : A \underset{1-1 onto}{⟶} B \to (((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \to \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w))$
31		simp3ll	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to x = H (z)$
32		simp1	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H : A \underset{1-1 onto}{⟶} B$
33		simp2l	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to z \in A$
34		f1of	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A ⟶ B$
35	34	ffvelrnda	$⊢ (H : A \underset{1-1 onto}{⟶} B \land z \in A) \to H (z) \in B$
36	32 33 35	syl2anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H (z) \in B$
37	31 36	eqeltrd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to x \in B$
38		simp3lr	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to y = H (w)$
39		simp2r	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to w \in A$
40	34	ffvelrnda	$⊢ (H : A \underset{1-1 onto}{⟶} B \land w \in A) \to H (w) \in B$
41	32 39 40	syl2anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H (w) \in B$
42	38 41	eqeltrd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to y \in B$
43		simp3r	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to z R w$
44	31	eqcomd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H (z) = x$
45		f1ocnvfv	$⊢ (H : A \underset{1-1 onto}{⟶} B \land z \in A) \to (H (z) = x \to H^{-1} (x) = z)$
46	32 33 45	syl2anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to (H (z) = x \to H^{-1} (x) = z)$
47	44 46	mpd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H^{-1} (x) = z$
48	38	eqcomd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H (w) = y$
49		f1ocnvfv	$⊢ (H : A \underset{1-1 onto}{⟶} B \land w \in A) \to (H (w) = y \to H^{-1} (y) = w)$
50	32 39 49	syl2anc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to (H (w) = y \to H^{-1} (y) = w)$
51	48 50	mpd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H^{-1} (y) = w$
52	43 47 51	3brtr4d	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to H^{-1} (x) R H^{-1} (y)$
53	37 42 52	jca31	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (z \in A \land w \in A) \land ((x = H (z) \land y = H (w)) \land z R w)) \to ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y))$
54	53	3exp	$⊢ H : A \underset{1-1 onto}{⟶} B \to ((z \in A \land w \in A) \to (((x = H (z) \land y = H (w)) \land z R w) \to ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y))))$
55	54	rexlimdvv	$⊢ H : A \underset{1-1 onto}{⟶} B \to (\exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w) \to ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)))$
56	30 55	impbid	$⊢ H : A \underset{1-1 onto}{⟶} B \to (((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y)) \leftrightarrow \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w))$
57	56	opabbidv	$⊢ H : A \underset{1-1 onto}{⟶} B \to \{⟨x, y⟩ \| ((x \in B \land y \in B) \land H^{-1} (x) R H^{-1} (y))\} = \{⟨x, y⟩ \| \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w)\}$
58	1 57	eqtrid	$⊢ H : A \underset{1-1 onto}{⟶} B \to S = \{⟨x, y⟩ \| \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w)\}$
59		f1oiso	$⊢ (H : A \underset{1-1 onto}{⟶} B \land S = \{⟨x, y⟩ \| \exists z \in A \exists w \in A ((x = H (z) \land y = H (w)) \land z R w)\}) \to H {Isom}_{R, S} (A, B)$
60	58 59	mpdan	$⊢ H : A \underset{1-1 onto}{⟶} B \to H {Isom}_{R, S} (A, B)$

Metamath Proof Explorer

Theorem f1oiso2

Proof