gpgprismgr4cycllem2

Description: Lemma 2 for gpgprismgr4cycl0 : the cycle <. P , F >. is proper, i.e., it has no overlapping edges. (Contributed by AV, 2-Nov-2025)

		Ref	Expression
	Hypothesis	gpgprismgr4cycllem1.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
	Assertion	gpgprismgr4cycllem2	$⊢ Fun F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycllem1.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
2		prex	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \in V$
3		prex	$⊢ \{⟨0, 1⟩, ⟨1, 1⟩\} \in V$
4	2 3	pm3.2i	$⊢ (\{⟨0, 0⟩, ⟨0, 1⟩\} \in V \land \{⟨0, 1⟩, ⟨1, 1⟩\} \in V)$
5		prex	$⊢ \{⟨1, 1⟩, ⟨1, 0⟩\} \in V$
6		prex	$⊢ \{⟨1, 0⟩, ⟨0, 0⟩\} \in V$
7	5 6	pm3.2i	$⊢ (\{⟨1, 1⟩, ⟨1, 0⟩\} \in V \land \{⟨1, 0⟩, ⟨0, 0⟩\} \in V)$
8	4 7	pm3.2i	$⊢ ((\{⟨0, 0⟩, ⟨0, 1⟩\} \in V \land \{⟨0, 1⟩, ⟨1, 1⟩\} \in V) \land (\{⟨1, 1⟩, ⟨1, 0⟩\} \in V \land \{⟨1, 0⟩, ⟨0, 0⟩\} \in V))$
9		opex	$⊢ ⟨0, 0⟩ \in V$
10		opex	$⊢ ⟨0, 1⟩ \in V$
11	9 10	pm3.2i	$⊢ (⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V)$
12		opex	$⊢ ⟨1, 1⟩ \in V$
13	10 12	pm3.2i	$⊢ (⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V)$
14	11 13	pm3.2i	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V))$
15		0ne1	$⊢ 0 \neq 1$
16	15	olci	$⊢ (0 \neq 0 \lor 0 \neq 1)$
17		c0ex	$⊢ 0 \in V$
18	17 17	opthne	$⊢ ⟨0, 0⟩ \neq ⟨0, 1⟩ \leftrightarrow (0 \neq 0 \lor 0 \neq 1)$
19	16 18	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨0, 1⟩$
20	15	orci	$⊢ (0 \neq 1 \lor 0 \neq 1)$
21	17 17	opthne	$⊢ ⟨0, 0⟩ \neq ⟨1, 1⟩ \leftrightarrow (0 \neq 1 \lor 0 \neq 1)$
22	20 21	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨1, 1⟩$
23	19 22	pm3.2i	$⊢ (⟨0, 0⟩ \neq ⟨0, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 1⟩)$
24	23	orci	$⊢ ((⟨0, 0⟩ \neq ⟨0, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 1⟩) \lor (⟨0, 1⟩ \neq ⟨0, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 1⟩))$
25		prneimg	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V)) \to (((⟨0, 0⟩ \neq ⟨0, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 1⟩) \lor (⟨0, 1⟩ \neq ⟨0, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 1⟩)) \to \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\})$
26	14 24 25	mp2	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\}$
27		opex	$⊢ ⟨1, 0⟩ \in V$
28	12 27	pm3.2i	$⊢ (⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V)$
29	11 28	pm3.2i	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V))$
30	15	orci	$⊢ (0 \neq 1 \lor 0 \neq 0)$
31	17 17	opthne	$⊢ ⟨0, 0⟩ \neq ⟨1, 0⟩ \leftrightarrow (0 \neq 1 \lor 0 \neq 0)$
32	30 31	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨1, 0⟩$
33	22 32	pm3.2i	$⊢ (⟨0, 0⟩ \neq ⟨1, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 0⟩)$
34	33	orci	$⊢ ((⟨0, 0⟩ \neq ⟨1, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 0⟩) \lor (⟨0, 1⟩ \neq ⟨1, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 0⟩))$
35		prneimg	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V)) \to (((⟨0, 0⟩ \neq ⟨1, 1⟩ \land ⟨0, 0⟩ \neq ⟨1, 0⟩) \lor (⟨0, 1⟩ \neq ⟨1, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 0⟩)) \to \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\})$
36	29 34 35	mp2	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\}$
37	27 9	pm3.2i	$⊢ (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V)$
38	11 37	pm3.2i	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V))$
39		ax-1ne0	$⊢ 1 \neq 0$
40	39	olci	$⊢ (0 \neq 1 \lor 1 \neq 0)$
41		1ex	$⊢ 1 \in V$
42	17 41	opthne	$⊢ ⟨0, 1⟩ \neq ⟨1, 0⟩ \leftrightarrow (0 \neq 1 \lor 1 \neq 0)$
43	40 42	mpbir	$⊢ ⟨0, 1⟩ \neq ⟨1, 0⟩$
44	39	olci	$⊢ (0 \neq 0 \lor 1 \neq 0)$
45	17 41	opthne	$⊢ ⟨0, 1⟩ \neq ⟨0, 0⟩ \leftrightarrow (0 \neq 0 \lor 1 \neq 0)$
46	44 45	mpbir	$⊢ ⟨0, 1⟩ \neq ⟨0, 0⟩$
47	43 46	pm3.2i	$⊢ (⟨0, 1⟩ \neq ⟨1, 0⟩ \land ⟨0, 1⟩ \neq ⟨0, 0⟩)$
48	47	olci	$⊢ ((⟨0, 0⟩ \neq ⟨1, 0⟩ \land ⟨0, 0⟩ \neq ⟨0, 0⟩) \lor (⟨0, 1⟩ \neq ⟨1, 0⟩ \land ⟨0, 1⟩ \neq ⟨0, 0⟩))$
49		prneimg	$⊢ ((⟨0, 0⟩ \in V \land ⟨0, 1⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V)) \to (((⟨0, 0⟩ \neq ⟨1, 0⟩ \land ⟨0, 0⟩ \neq ⟨0, 0⟩) \lor (⟨0, 1⟩ \neq ⟨1, 0⟩ \land ⟨0, 1⟩ \neq ⟨0, 0⟩)) \to \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})$
50	38 48 49	mp2	$⊢ \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}$
51	26 36 50	3pm3.2i	$⊢ (\{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})$
52	13 28	pm3.2i	$⊢ ((⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V))$
53	15	orci	$⊢ (0 \neq 1 \lor 1 \neq 1)$
54	17 41	opthne	$⊢ ⟨0, 1⟩ \neq ⟨1, 1⟩ \leftrightarrow (0 \neq 1 \lor 1 \neq 1)$
55	53 54	mpbir	$⊢ ⟨0, 1⟩ \neq ⟨1, 1⟩$
56	55 43	pm3.2i	$⊢ (⟨0, 1⟩ \neq ⟨1, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 0⟩)$
57	56	orci	$⊢ ((⟨0, 1⟩ \neq ⟨1, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 0⟩) \lor (⟨1, 1⟩ \neq ⟨1, 1⟩ \land ⟨1, 1⟩ \neq ⟨1, 0⟩))$
58		prneimg	$⊢ ((⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V) \land (⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V)) \to (((⟨0, 1⟩ \neq ⟨1, 1⟩ \land ⟨0, 1⟩ \neq ⟨1, 0⟩) \lor (⟨1, 1⟩ \neq ⟨1, 1⟩ \land ⟨1, 1⟩ \neq ⟨1, 0⟩)) \to \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\})$
59	52 57 58	mp2	$⊢ \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\}$
60	13 37	pm3.2i	$⊢ ((⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V))$
61	39	olci	$⊢ (1 \neq 1 \lor 1 \neq 0)$
62	41 41	opthne	$⊢ ⟨1, 1⟩ \neq ⟨1, 0⟩ \leftrightarrow (1 \neq 1 \lor 1 \neq 0)$
63	61 62	mpbir	$⊢ ⟨1, 1⟩ \neq ⟨1, 0⟩$
64	39	olci	$⊢ (1 \neq 0 \lor 1 \neq 0)$
65	41 41	opthne	$⊢ ⟨1, 1⟩ \neq ⟨0, 0⟩ \leftrightarrow (1 \neq 0 \lor 1 \neq 0)$
66	64 65	mpbir	$⊢ ⟨1, 1⟩ \neq ⟨0, 0⟩$
67	63 66	pm3.2i	$⊢ (⟨1, 1⟩ \neq ⟨1, 0⟩ \land ⟨1, 1⟩ \neq ⟨0, 0⟩)$
68	67	olci	$⊢ ((⟨0, 1⟩ \neq ⟨1, 0⟩ \land ⟨0, 1⟩ \neq ⟨0, 0⟩) \lor (⟨1, 1⟩ \neq ⟨1, 0⟩ \land ⟨1, 1⟩ \neq ⟨0, 0⟩))$
69		prneimg	$⊢ ((⟨0, 1⟩ \in V \land ⟨1, 1⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V)) \to (((⟨0, 1⟩ \neq ⟨1, 0⟩ \land ⟨0, 1⟩ \neq ⟨0, 0⟩) \lor (⟨1, 1⟩ \neq ⟨1, 0⟩ \land ⟨1, 1⟩ \neq ⟨0, 0⟩)) \to \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})$
70	60 68 69	mp2	$⊢ \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}$
71	28 37	pm3.2i	$⊢ ((⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V))$
72	67	orci	$⊢ ((⟨1, 1⟩ \neq ⟨1, 0⟩ \land ⟨1, 1⟩ \neq ⟨0, 0⟩) \lor (⟨1, 0⟩ \neq ⟨1, 0⟩ \land ⟨1, 0⟩ \neq ⟨0, 0⟩))$
73		prneimg	$⊢ ((⟨1, 1⟩ \in V \land ⟨1, 0⟩ \in V) \land (⟨1, 0⟩ \in V \land ⟨0, 0⟩ \in V)) \to (((⟨1, 1⟩ \neq ⟨1, 0⟩ \land ⟨1, 1⟩ \neq ⟨0, 0⟩) \lor (⟨1, 0⟩ \neq ⟨1, 0⟩ \land ⟨1, 0⟩ \neq ⟨0, 0⟩)) \to \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})$
74	71 72 73	mp2	$⊢ \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}$
75	59 70 74	3pm3.2i	$⊢ (\{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\} \land \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})$
76	51 75	pm3.2i	$⊢ ((\{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}) \land (\{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\} \land \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}))$
77	8 76	pm3.2i	$⊢ (((\{⟨0, 0⟩, ⟨0, 1⟩\} \in V \land \{⟨0, 1⟩, ⟨1, 1⟩\} \in V) \land (\{⟨1, 1⟩, ⟨1, 0⟩\} \in V \land \{⟨1, 0⟩, ⟨0, 0⟩\} \in V)) \land ((\{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}) \land (\{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\} \land \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})))$
78		s4f1o	$⊢ ((\{⟨0, 0⟩, ⟨0, 1⟩\} \in V \land \{⟨0, 1⟩, ⟨1, 1⟩\} \in V) \land (\{⟨1, 1⟩, ⟨1, 0⟩\} \in V \land \{⟨1, 0⟩, ⟨0, 0⟩\} \in V)) \to (((\{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}) \land (\{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\} \land \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\})) \to (F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}))$
79	78	imp	$⊢ (((\{⟨0, 0⟩, ⟨0, 1⟩\} \in V \land \{⟨0, 1⟩, ⟨1, 1⟩\} \in V) \land (\{⟨1, 1⟩, ⟨1, 0⟩\} \in V \land \{⟨1, 0⟩, ⟨0, 0⟩\} \in V)) \land ((\{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨0, 1⟩, ⟨1, 1⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 0⟩, ⟨0, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}) \land (\{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 1⟩, ⟨1, 0⟩\} \land \{⟨0, 1⟩, ⟨1, 1⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\} \land \{⟨1, 1⟩, ⟨1, 0⟩\} \neq \{⟨1, 0⟩, ⟨0, 0⟩\}))) \to (F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\})$
80		pm2.27	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to ((F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}) \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\})$
81	1 80	ax-mp	$⊢ (F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}) \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}$
82		df-f1o	$⊢ F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \leftrightarrow (F : dom F \underset{1-1}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \land F : dom F \underset{onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\})$
83		df-f1	$⊢ F : dom F \underset{1-1}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \leftrightarrow (F : dom F ⟶ \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \land Fun F^{-1})$
84	83	simprbi	$⊢ F : dom F \underset{1-1}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \to Fun F^{-1}$
85	84	adantr	$⊢ (F : dom F \underset{1-1}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \land F : dom F \underset{onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}) \to Fun F^{-1}$
86	82 85	sylbi	$⊢ F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\} \to Fun F^{-1}$
87	81 86	syl	$⊢ (F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩ \to F : dom F \underset{1-1 onto}{⟶} \{\{⟨0, 0⟩, ⟨0, 1⟩\}, \{⟨0, 1⟩, ⟨1, 1⟩\}\} \cup \{\{⟨1, 1⟩, ⟨1, 0⟩\}, \{⟨1, 0⟩, ⟨0, 0⟩\}\}) \to Fun F^{-1}$
88	77 79 87	mp2b	$⊢ Fun F^{-1}$

Metamath Proof Explorer

Theorem gpgprismgr4cycllem2

Proof