isocnv3

Description: Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypotheses	isocnv3.1	$⊢ C = (A \times A) ∖ R$
	isocnv3.2	$⊢ D = (B \times B) ∖ S$
Assertion	isocnv3	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow H {Isom}_{C, D} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		isocnv3.1	$⊢ C = (A \times A) ∖ R$
2		isocnv3.2	$⊢ D = (B \times B) ∖ S$
3		notbi	$⊢ (x R y \leftrightarrow H (x) S H (y)) \leftrightarrow (\neg x R y \leftrightarrow \neg H (x) S H (y))$
4		brxp	$⊢ x (A \times A) y \leftrightarrow (x \in A \land y \in A)$
5	1	breqi	$⊢ x C y \leftrightarrow x ((A \times A) ∖ R) y$
6		brdif	$⊢ x ((A \times A) ∖ R) y \leftrightarrow (x (A \times A) y \land \neg x R y)$
7	5 6	bitri	$⊢ x C y \leftrightarrow (x (A \times A) y \land \neg x R y)$
8	7	baib	$⊢ x (A \times A) y \to (x C y \leftrightarrow \neg x R y)$
9	4 8	sylbir	$⊢ (x \in A \land y \in A) \to (x C y \leftrightarrow \neg x R y)$
10	9	adantl	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (x C y \leftrightarrow \neg x R y)$
11		f1of	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A ⟶ B$
12		ffvelrn	$⊢ (H : A ⟶ B \land x \in A) \to H (x) \in B$
13		ffvelrn	$⊢ (H : A ⟶ B \land y \in A) \to H (y) \in B$
14	12 13	anim12dan	$⊢ (H : A ⟶ B \land (x \in A \land y \in A)) \to (H (x) \in B \land H (y) \in B)$
15		brxp	$⊢ H (x) (B \times B) H (y) \leftrightarrow (H (x) \in B \land H (y) \in B)$
16	14 15	sylibr	$⊢ (H : A ⟶ B \land (x \in A \land y \in A)) \to H (x) (B \times B) H (y)$
17	11 16	sylan	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to H (x) (B \times B) H (y)$
18	2	breqi	$⊢ H (x) D H (y) \leftrightarrow H (x) ((B \times B) ∖ S) H (y)$
19		brdif	$⊢ H (x) ((B \times B) ∖ S) H (y) \leftrightarrow (H (x) (B \times B) H (y) \land \neg H (x) S H (y))$
20	18 19	bitri	$⊢ H (x) D H (y) \leftrightarrow (H (x) (B \times B) H (y) \land \neg H (x) S H (y))$
21	20	baib	$⊢ H (x) (B \times B) H (y) \to (H (x) D H (y) \leftrightarrow \neg H (x) S H (y))$
22	17 21	syl	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (H (x) D H (y) \leftrightarrow \neg H (x) S H (y))$
23	10 22	bibi12d	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to ((x C y \leftrightarrow H (x) D H (y)) \leftrightarrow (\neg x R y \leftrightarrow \neg H (x) S H (y)))$
24	3 23	bitr4id	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to ((x R y \leftrightarrow H (x) S H (y)) \leftrightarrow (x C y \leftrightarrow H (x) D H (y)))$
25	24	2ralbidva	$⊢ H : A \underset{1-1 onto}{⟶} B \to (\forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)) \leftrightarrow \forall x \in A \forall y \in A (x C y \leftrightarrow H (x) D H (y)))$
26	25	pm5.32i	$⊢ (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x C y \leftrightarrow H (x) D H (y)))$
27		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)))$
28		df-isom	$⊢ H {Isom}_{C, D} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x C y \leftrightarrow H (x) D H (y)))$
29	26 27 28	3bitr4i	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow H {Isom}_{C, D} (A, B)$

Metamath Proof Explorer

Theorem isocnv3

Proof