fpropnf1

Description: A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021)

		Ref	Expression
	Hypothesis	fpropnf1.f	$⊢ F = \{⟨X, Z⟩, ⟨Y, Z⟩\}$
	Assertion	fpropnf1	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (Fun F \land \neg Fun F^{-1})$

Proof

Step	Hyp	Ref	Expression
1		fpropnf1.f	$⊢ F = \{⟨X, Z⟩, ⟨Y, Z⟩\}$
2		id	$⊢ (X \in U \land Y \in V) \to (X \in U \land Y \in V)$
3	2	3adant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to (X \in U \land Y \in V)$
4	3	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (X \in U \land Y \in V)$
5		id	$⊢ Z \in W \to Z \in W$
6	5 5	jca	$⊢ Z \in W \to (Z \in W \land Z \in W)$
7	6	3ad2ant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to (Z \in W \land Z \in W)$
8	7	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (Z \in W \land Z \in W)$
9		simpr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to X \neq Y$
10	4 8 9	3jca	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((X \in U \land Y \in V) \land (Z \in W \land Z \in W) \land X \neq Y)$
11		funprg	$⊢ ((X \in U \land Y \in V) \land (Z \in W \land Z \in W) \land X \neq Y) \to Fun \{⟨X, Z⟩, ⟨Y, Z⟩\}$
12	10 11	syl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to Fun \{⟨X, Z⟩, ⟨Y, Z⟩\}$
13	1	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨X, Z⟩, ⟨Y, Z⟩\}$
14	12 13	sylibr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to Fun F$
15		neneq	$⊢ X \neq Y \to \neg X = Y$
16	15	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to \neg X = Y$
17		fprg	$⊢ ((X \in U \land Y \in V) \land (Z \in W \land Z \in W) \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} : \{X, Y\} ⟶ \{Z, Z\}$
18	10 17	syl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} : \{X, Y\} ⟶ \{Z, Z\}$
19	1	eqcomi	$⊢ \{⟨X, Z⟩, ⟨Y, Z⟩\} = F$
20	19	feq1i	$⊢ \{⟨X, Z⟩, ⟨Y, Z⟩\} : \{X, Y\} ⟶ \{Z, Z\} \leftrightarrow F : \{X, Y\} ⟶ \{Z, Z\}$
21	18 20	sylib	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to F : \{X, Y\} ⟶ \{Z, Z\}$
22		df-f1	$⊢ F : \{X, Y\} \underset{1-1}{⟶} \{Z, Z\} \leftrightarrow (F : \{X, Y\} ⟶ \{Z, Z\} \land Fun F^{-1})$
23		dff13	$⊢ F : \{X, Y\} \underset{1-1}{⟶} \{Z, Z\} \leftrightarrow (F : \{X, Y\} ⟶ \{Z, Z\} \land \forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y))$
24		fveqeq2	$⊢ x = X \to (F (x) = F (y) \leftrightarrow F (X) = F (y))$
25		eqeq1	$⊢ x = X \to (x = y \leftrightarrow X = y)$
26	24 25	imbi12d	$⊢ x = X \to ((F (x) = F (y) \to x = y) \leftrightarrow (F (X) = F (y) \to X = y))$
27	26	ralbidv	$⊢ x = X \to (\forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \leftrightarrow \forall y \in \{X, Y\} (F (X) = F (y) \to X = y))$
28		fveqeq2	$⊢ x = Y \to (F (x) = F (y) \leftrightarrow F (Y) = F (y))$
29		eqeq1	$⊢ x = Y \to (x = y \leftrightarrow Y = y)$
30	28 29	imbi12d	$⊢ x = Y \to ((F (x) = F (y) \to x = y) \leftrightarrow (F (Y) = F (y) \to Y = y))$
31	30	ralbidv	$⊢ x = Y \to (\forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \leftrightarrow \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y))$
32	27 31	ralprg	$⊢ (X \in U \land Y \in V) \to (\forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \leftrightarrow (\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)))$
33	32	3adant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to (\forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \leftrightarrow (\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)))$
34	33	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (\forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \leftrightarrow (\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)))$
35		fveq2	$⊢ y = X \to F (y) = F (X)$
36	35	eqeq2d	$⊢ y = X \to (F (X) = F (y) \leftrightarrow F (X) = F (X))$
37		eqeq2	$⊢ y = X \to (X = y \leftrightarrow X = X)$
38	36 37	imbi12d	$⊢ y = X \to ((F (X) = F (y) \to X = y) \leftrightarrow (F (X) = F (X) \to X = X))$
39		fveq2	$⊢ y = Y \to F (y) = F (Y)$
40	39	eqeq2d	$⊢ y = Y \to (F (X) = F (y) \leftrightarrow F (X) = F (Y))$
41		eqeq2	$⊢ y = Y \to (X = y \leftrightarrow X = Y)$
42	40 41	imbi12d	$⊢ y = Y \to ((F (X) = F (y) \to X = y) \leftrightarrow (F (X) = F (Y) \to X = Y))$
43	38 42	ralprg	$⊢ (X \in U \land Y \in V) \to (\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \leftrightarrow ((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)))$
44	35	eqeq2d	$⊢ y = X \to (F (Y) = F (y) \leftrightarrow F (Y) = F (X))$
45		eqeq2	$⊢ y = X \to (Y = y \leftrightarrow Y = X)$
46	44 45	imbi12d	$⊢ y = X \to ((F (Y) = F (y) \to Y = y) \leftrightarrow (F (Y) = F (X) \to Y = X))$
47	39	eqeq2d	$⊢ y = Y \to (F (Y) = F (y) \leftrightarrow F (Y) = F (Y))$
48		eqeq2	$⊢ y = Y \to (Y = y \leftrightarrow Y = Y)$
49	47 48	imbi12d	$⊢ y = Y \to ((F (Y) = F (y) \to Y = y) \leftrightarrow (F (Y) = F (Y) \to Y = Y))$
50	46 49	ralprg	$⊢ (X \in U \land Y \in V) \to (\forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y) \leftrightarrow ((F (Y) = F (X) \to Y = X) \land (F (Y) = F (Y) \to Y = Y)))$
51	43 50	anbi12d	$⊢ (X \in U \land Y \in V) \to ((\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)) \leftrightarrow (((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)) \land ((F (Y) = F (X) \to Y = X) \land (F (Y) = F (Y) \to Y = Y))))$
52	51	3adant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to ((\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)) \leftrightarrow (((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)) \land ((F (Y) = F (X) \to Y = X) \land (F (Y) = F (Y) \to Y = Y))))$
53	52	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)) \leftrightarrow (((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)) \land ((F (Y) = F (X) \to Y = X) \land (F (Y) = F (Y) \to Y = Y))))$
54	1	fveq1i	$⊢ F (X) = \{⟨X, Z⟩, ⟨Y, Z⟩\} (X)$
55		3simpb	$⊢ (X \in U \land Y \in V \land Z \in W) \to (X \in U \land Z \in W)$
56	55	anim1i	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((X \in U \land Z \in W) \land X \neq Y)$
57		df-3an	$⊢ (X \in U \land Z \in W \land X \neq Y) \leftrightarrow ((X \in U \land Z \in W) \land X \neq Y)$
58	56 57	sylibr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (X \in U \land Z \in W \land X \neq Y)$
59		fvpr1g	$⊢ (X \in U \land Z \in W \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} (X) = Z$
60	58 59	syl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} (X) = Z$
61	54 60	syl5eq	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to F (X) = Z$
62	1	fveq1i	$⊢ F (Y) = \{⟨X, Z⟩, ⟨Y, Z⟩\} (Y)$
63		3simpc	$⊢ (X \in U \land Y \in V \land Z \in W) \to (Y \in V \land Z \in W)$
64	63	anim1i	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((Y \in V \land Z \in W) \land X \neq Y)$
65		df-3an	$⊢ (Y \in V \land Z \in W \land X \neq Y) \leftrightarrow ((Y \in V \land Z \in W) \land X \neq Y)$
66	64 65	sylibr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (Y \in V \land Z \in W \land X \neq Y)$
67		fvpr2g	$⊢ (Y \in V \land Z \in W \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} (Y) = Z$
68	66 67	syl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to \{⟨X, Z⟩, ⟨Y, Z⟩\} (Y) = Z$
69	62 68	syl5req	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to Z = F (Y)$
70	61 69	eqtrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to F (X) = F (Y)$
71		idd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (X = Y \to X = Y)$
72	70 71	embantd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((F (X) = F (Y) \to X = Y) \to X = Y)$
73	72	adantld	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)) \to X = Y)$
74	73	adantrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((((F (X) = F (X) \to X = X) \land (F (X) = F (Y) \to X = Y)) \land ((F (Y) = F (X) \to Y = X) \land (F (Y) = F (Y) \to Y = Y))) \to X = Y)$
75	53 74	sylbid	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((\forall y \in \{X, Y\} (F (X) = F (y) \to X = y) \land \forall y \in \{X, Y\} (F (Y) = F (y) \to Y = y)) \to X = Y)$
76	34 75	sylbid	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (\forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y) \to X = Y)$
77	76	adantld	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((F : \{X, Y\} ⟶ \{Z, Z\} \land \forall x \in \{X, Y\} \forall y \in \{X, Y\} (F (x) = F (y) \to x = y)) \to X = Y)$
78	23 77	syl5bi	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (F : \{X, Y\} \underset{1-1}{⟶} \{Z, Z\} \to X = Y)$
79	22 78	syl5bir	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to ((F : \{X, Y\} ⟶ \{Z, Z\} \land Fun F^{-1}) \to X = Y)$
80	21 79	mpand	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (Fun F^{-1} \to X = Y)$
81	16 80	mtod	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to \neg Fun F^{-1}$
82	14 81	jca	$⊢ ((X \in U \land Y \in V \land Z \in W) \land X \neq Y) \to (Fun F \land \neg Fun F^{-1})$

Metamath Proof Explorer

Theorem fpropnf1

Proof