disjf1

Description: A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	disjf1.xph	$⊢ Ⅎ x φ$
	disjf1.f	$⊢ F = (x \in A ⟼ B)$
	disjf1.b	$⊢ (φ \land x \in A) \to B \in V$
	disjf1.n0	$⊢ (φ \land x \in A) \to B \neq \emptyset$
	disjf1.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
Assertion	disjf1	$⊢ φ \to F : A \underset{1-1}{⟶} V$

Proof

Step	Hyp	Ref	Expression
1		disjf1.xph	$⊢ Ⅎ x φ$
2		disjf1.f	$⊢ F = (x \in A ⟼ B)$
3		disjf1.b	$⊢ (φ \land x \in A) \to B \in V$
4		disjf1.n0	$⊢ (φ \land x \in A) \to B \neq \emptyset$
5		disjf1.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
6		nfv	$⊢ Ⅎ x y \in A$
7	1 6	nfan	$⊢ Ⅎ x (φ \land y \in A)$
8		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
9		nfcv	$⊢ \underline{Ⅎ} x V$
10	8 9	nfel	$⊢ Ⅎ x ⦋ y / x ⦌ B \in V$
11	7 10	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to ⦋ y / x ⦌ B \in V)$
12		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
13	12	anbi2d	$⊢ x = y \to ((φ \land x \in A) \leftrightarrow (φ \land y \in A))$
14		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
15	14	eleq1d	$⊢ x = y \to (B \in V \leftrightarrow ⦋ y / x ⦌ B \in V)$
16	13 15	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to B \in V) \leftrightarrow ((φ \land y \in A) \to ⦋ y / x ⦌ B \in V))$
17	11 16 3	chvarfv	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \in V$
18	17	ralrimiva	$⊢ φ \to \forall y \in A ⦋ y / x ⦌ B \in V$
19		inidm	$⊢ ⦋ y / x ⦌ B \cap ⦋ y / x ⦌ B = ⦋ y / x ⦌ B$
20	19	eqcomi	$⊢ ⦋ y / x ⦌ B = ⦋ y / x ⦌ B \cap ⦋ y / x ⦌ B$
21	20	a1i	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to ⦋ y / x ⦌ B = ⦋ y / x ⦌ B \cap ⦋ y / x ⦌ B$
22		ineq2	$⊢ ⦋ y / x ⦌ B = ⦋ z / x ⦌ B \to ⦋ y / x ⦌ B \cap ⦋ y / x ⦌ B = ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B$
23	22	ad2antlr	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to ⦋ y / x ⦌ B \cap ⦋ y / x ⦌ B = ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B$
24		nfcv	$⊢ \underline{Ⅎ} w B$
25		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
26		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
27	24 25 26	cbvdisj	$⊢ \underset{x \in A}{Disj} B \leftrightarrow \underset{w \in A}{Disj} ⦋ w / x ⦌ B$
28	5 27	sylib	$⊢ φ \to \underset{w \in A}{Disj} ⦋ w / x ⦌ B$
29	28	ad3antrrr	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to \underset{w \in A}{Disj} ⦋ w / x ⦌ B$
30		simpllr	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to (y \in A \land z \in A)$
31		neqne	$⊢ \neg y = z \to y \neq z$
32	31	adantl	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to y \neq z$
33		csbeq1	$⊢ w = y \to ⦋ w / x ⦌ B = ⦋ y / x ⦌ B$
34		csbeq1	$⊢ w = z \to ⦋ w / x ⦌ B = ⦋ z / x ⦌ B$
35	33 34	disji2	$⊢ (\underset{w \in A}{Disj} ⦋ w / x ⦌ B \land (y \in A \land z \in A) \land y \neq z) \to ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset$
36	29 30 32 35	syl3anc	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to ⦋ y / x ⦌ B \cap ⦋ z / x ⦌ B = \emptyset$
37	21 23 36	3eqtrd	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to ⦋ y / x ⦌ B = \emptyset$
38		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
39	8 38	nfne	$⊢ Ⅎ x ⦋ y / x ⦌ B \neq \emptyset$
40	7 39	nfim	$⊢ Ⅎ x ((φ \land y \in A) \to ⦋ y / x ⦌ B \neq \emptyset)$
41	14	neeq1d	$⊢ x = y \to (B \neq \emptyset \leftrightarrow ⦋ y / x ⦌ B \neq \emptyset)$
42	13 41	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to B \neq \emptyset) \leftrightarrow ((φ \land y \in A) \to ⦋ y / x ⦌ B \neq \emptyset))$
43	40 42 4	chvarfv	$⊢ (φ \land y \in A) \to ⦋ y / x ⦌ B \neq \emptyset$
44	43	adantrr	$⊢ (φ \land (y \in A \land z \in A)) \to ⦋ y / x ⦌ B \neq \emptyset$
45	44	ad2antrr	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to ⦋ y / x ⦌ B \neq \emptyset$
46	45	neneqd	$⊢ (((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \land \neg y = z) \to \neg ⦋ y / x ⦌ B = \emptyset$
47	37 46	condan	$⊢ ((φ \land (y \in A \land z \in A)) \land ⦋ y / x ⦌ B = ⦋ z / x ⦌ B) \to y = z$
48	47	ex	$⊢ (φ \land (y \in A \land z \in A)) \to (⦋ y / x ⦌ B = ⦋ z / x ⦌ B \to y = z)$
49	48	ralrimivva	$⊢ φ \to \forall y \in A \forall z \in A (⦋ y / x ⦌ B = ⦋ z / x ⦌ B \to y = z)$
50	18 49	jca	$⊢ φ \to (\forall y \in A ⦋ y / x ⦌ B \in V \land \forall y \in A \forall z \in A (⦋ y / x ⦌ B = ⦋ z / x ⦌ B \to y = z))$
51		nfcv	$⊢ \underline{Ⅎ} y B$
52	51 8 14	cbvmpt	$⊢ (x \in A ⟼ B) = (y \in A ⟼ ⦋ y / x ⦌ B)$
53	2 52	eqtri	$⊢ F = (y \in A ⟼ ⦋ y / x ⦌ B)$
54		csbeq1	$⊢ y = z \to ⦋ y / x ⦌ B = ⦋ z / x ⦌ B$
55	53 54	f1mpt	$⊢ F : A \underset{1-1}{⟶} V \leftrightarrow (\forall y \in A ⦋ y / x ⦌ B \in V \land \forall y \in A \forall z \in A (⦋ y / x ⦌ B = ⦋ z / x ⦌ B \to y = z))$
56	50 55	sylibr	$⊢ φ \to F : A \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem disjf1

Proof