f1oiso

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . Proposition 6.33 of TakeutiZaring p. 34. (Contributed by NM, 30-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (H : A \underset{1-1 onto}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \to H : A \underset{1-1 onto}{⟶} B$
2		f1of1	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{1-1}{⟶} B$
3		df-br	$⊢ H (v) S H (u) \leftrightarrow ⟨H (v), H (u)⟩ \in S$
4		eleq2	$⊢ S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\} \to (⟨H (v), H (u)⟩ \in S \leftrightarrow ⟨H (v), H (u)⟩ \in \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\})$
5		fvex	$⊢ H (v) \in V$
6		fvex	$⊢ H (u) \in V$
7		eqeq1	$⊢ z = H (v) \to (z = H (x) \leftrightarrow H (v) = H (x))$
8	7	anbi1d	$⊢ z = H (v) \to ((z = H (x) \land w = H (y)) \leftrightarrow (H (v) = H (x) \land w = H (y)))$
9	8	anbi1d	$⊢ z = H (v) \to (((z = H (x) \land w = H (y)) \land x R y) \leftrightarrow ((H (v) = H (x) \land w = H (y)) \land x R y))$
10	9	2rexbidv	$⊢ z = H (v) \to (\exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y) \leftrightarrow \exists x \in A \exists y \in A ((H (v) = H (x) \land w = H (y)) \land x R y))$
11		eqeq1	$⊢ w = H (u) \to (w = H (y) \leftrightarrow H (u) = H (y))$
12	11	anbi2d	$⊢ w = H (u) \to ((H (v) = H (x) \land w = H (y)) \leftrightarrow (H (v) = H (x) \land H (u) = H (y)))$
13	12	anbi1d	$⊢ w = H (u) \to (((H (v) = H (x) \land w = H (y)) \land x R y) \leftrightarrow ((H (v) = H (x) \land H (u) = H (y)) \land x R y))$
14	13	2rexbidv	$⊢ w = H (u) \to (\exists x \in A \exists y \in A ((H (v) = H (x) \land w = H (y)) \land x R y) \leftrightarrow \exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y))$
15	5 6 10 14	opelopab	$⊢ ⟨H (v), H (u)⟩ \in \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\} \leftrightarrow \exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y)$
16		anass	$⊢ ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow (H (v) = H (x) \land (H (u) = H (y) \land x R y))$
17		f1fveq	$⊢ (H : A \underset{1-1}{⟶} B \land (v \in A \land x \in A)) \to (H (v) = H (x) \leftrightarrow v = x)$
18		equcom	$⊢ v = x \leftrightarrow x = v$
19	17 18	bitrdi	$⊢ (H : A \underset{1-1}{⟶} B \land (v \in A \land x \in A)) \to (H (v) = H (x) \leftrightarrow x = v)$
20	19	anassrs	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land x \in A) \to (H (v) = H (x) \leftrightarrow x = v)$
21	20	anbi1d	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land x \in A) \to ((H (v) = H (x) \land (H (u) = H (y) \land x R y)) \leftrightarrow (x = v \land (H (u) = H (y) \land x R y)))$
22	16 21	syl5bb	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land x \in A) \to (((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow (x = v \land (H (u) = H (y) \land x R y)))$
23	22	rexbidv	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land x \in A) \to (\exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow \exists y \in A (x = v \land (H (u) = H (y) \land x R y)))$
24		r19.42v	$⊢ \exists y \in A (x = v \land (H (u) = H (y) \land x R y)) \leftrightarrow (x = v \land \exists y \in A (H (u) = H (y) \land x R y))$
25	23 24	bitrdi	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land x \in A) \to (\exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow (x = v \land \exists y \in A (H (u) = H (y) \land x R y)))$
26	25	rexbidva	$⊢ (H : A \underset{1-1}{⟶} B \land v \in A) \to (\exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow \exists x \in A (x = v \land \exists y \in A (H (u) = H (y) \land x R y)))$
27		breq1	$⊢ x = v \to (x R y \leftrightarrow v R y)$
28	27	anbi2d	$⊢ x = v \to ((H (u) = H (y) \land x R y) \leftrightarrow (H (u) = H (y) \land v R y))$
29	28	rexbidv	$⊢ x = v \to (\exists y \in A (H (u) = H (y) \land x R y) \leftrightarrow \exists y \in A (H (u) = H (y) \land v R y))$
30	29	ceqsrexv	$⊢ v \in A \to (\exists x \in A (x = v \land \exists y \in A (H (u) = H (y) \land x R y)) \leftrightarrow \exists y \in A (H (u) = H (y) \land v R y))$
31	30	adantl	$⊢ (H : A \underset{1-1}{⟶} B \land v \in A) \to (\exists x \in A (x = v \land \exists y \in A (H (u) = H (y) \land x R y)) \leftrightarrow \exists y \in A (H (u) = H (y) \land v R y))$
32	26 31	bitrd	$⊢ (H : A \underset{1-1}{⟶} B \land v \in A) \to (\exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow \exists y \in A (H (u) = H (y) \land v R y))$
33		f1fveq	$⊢ (H : A \underset{1-1}{⟶} B \land (u \in A \land y \in A)) \to (H (u) = H (y) \leftrightarrow u = y)$
34		equcom	$⊢ u = y \leftrightarrow y = u$
35	33 34	bitrdi	$⊢ (H : A \underset{1-1}{⟶} B \land (u \in A \land y \in A)) \to (H (u) = H (y) \leftrightarrow y = u)$
36	35	anassrs	$⊢ ((H : A \underset{1-1}{⟶} B \land u \in A) \land y \in A) \to (H (u) = H (y) \leftrightarrow y = u)$
37	36	anbi1d	$⊢ ((H : A \underset{1-1}{⟶} B \land u \in A) \land y \in A) \to ((H (u) = H (y) \land v R y) \leftrightarrow (y = u \land v R y))$
38	37	rexbidva	$⊢ (H : A \underset{1-1}{⟶} B \land u \in A) \to (\exists y \in A (H (u) = H (y) \land v R y) \leftrightarrow \exists y \in A (y = u \land v R y))$
39		breq2	$⊢ y = u \to (v R y \leftrightarrow v R u)$
40	39	ceqsrexv	$⊢ u \in A \to (\exists y \in A (y = u \land v R y) \leftrightarrow v R u)$
41	40	adantl	$⊢ (H : A \underset{1-1}{⟶} B \land u \in A) \to (\exists y \in A (y = u \land v R y) \leftrightarrow v R u)$
42	38 41	bitrd	$⊢ (H : A \underset{1-1}{⟶} B \land u \in A) \to (\exists y \in A (H (u) = H (y) \land v R y) \leftrightarrow v R u)$
43	32 42	sylan9bb	$⊢ ((H : A \underset{1-1}{⟶} B \land v \in A) \land (H : A \underset{1-1}{⟶} B \land u \in A)) \to (\exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow v R u)$
44	43	anandis	$⊢ (H : A \underset{1-1}{⟶} B \land (v \in A \land u \in A)) \to (\exists x \in A \exists y \in A ((H (v) = H (x) \land H (u) = H (y)) \land x R y) \leftrightarrow v R u)$
45	15 44	syl5bb	$⊢ (H : A \underset{1-1}{⟶} B \land (v \in A \land u \in A)) \to (⟨H (v), H (u)⟩ \in \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\} \leftrightarrow v R u)$
46	4 45	sylan9bbr	$⊢ ((H : A \underset{1-1}{⟶} B \land (v \in A \land u \in A)) \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \to (⟨H (v), H (u)⟩ \in S \leftrightarrow v R u)$
47	46	an32s	$⊢ ((H : A \underset{1-1}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \land (v \in A \land u \in A)) \to (⟨H (v), H (u)⟩ \in S \leftrightarrow v R u)$
48	3 47	bitr2id	$⊢ ((H : A \underset{1-1}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \land (v \in A \land u \in A)) \to (v R u \leftrightarrow H (v) S H (u))$
49	48	ralrimivva	$⊢ (H : A \underset{1-1}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \to \forall v \in A \forall u \in A (v R u \leftrightarrow H (v) S H (u))$
50	2 49	sylan	$⊢ (H : A \underset{1-1 onto}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \to \forall v \in A \forall u \in A (v R u \leftrightarrow H (v) S H (u))$
51		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall v \in A \forall u \in A (v R u \leftrightarrow H (v) S H (u)))$
52	1 50 51	sylanbrc	$⊢ (H : A \underset{1-1 onto}{⟶} B \land S = \{⟨z, w⟩ \| \exists x \in A \exists y \in A ((z = H (x) \land w = H (y)) \land x R y)\}) \to H {Isom}_{R, S} (A, B)$

Metamath Proof Explorer

Theorem f1oiso

Proof