disjf1o

Description: A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	disjf1o.xph	$⊢ Ⅎ x φ$
	disjf1o.f	$⊢ F = (x \in A ⟼ B)$
	disjf1o.b	$⊢ (φ \land x \in A) \to B \in V$
	disjf1o.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
	disjf1o.d	$⊢ C = \{x \in A \| B \neq \emptyset\}$
	disjf1o.e	$⊢ D = ran F ∖ \{\emptyset\}$
Assertion	disjf1o	$⊢ φ \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		disjf1o.xph	$⊢ Ⅎ x φ$
2		disjf1o.f	$⊢ F = (x \in A ⟼ B)$
3		disjf1o.b	$⊢ (φ \land x \in A) \to B \in V$
4		disjf1o.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
5		disjf1o.d	$⊢ C = \{x \in A \| B \neq \emptyset\}$
6		disjf1o.e	$⊢ D = ran F ∖ \{\emptyset\}$
7		eqid	$⊢ (x \in C ⟼ B) = (x \in C ⟼ B)$
8		simpl	$⊢ (φ \land x \in C) \to φ$
9		ssrab2	$⊢ \{x \in A \| B \neq \emptyset\} \subseteq A$
10	5 9	eqsstri	$⊢ C \subseteq A$
11		id	$⊢ x \in C \to x \in C$
12	10 11	sselid	$⊢ x \in C \to x \in A$
13	12	adantl	$⊢ (φ \land x \in C) \to x \in A$
14	8 13 3	syl2anc	$⊢ (φ \land x \in C) \to B \in V$
15	11 5	eleqtrdi	$⊢ x \in C \to x \in \{x \in A \| B \neq \emptyset\}$
16		rabid	$⊢ x \in \{x \in A \| B \neq \emptyset\} \leftrightarrow (x \in A \land B \neq \emptyset)$
17	16	a1i	$⊢ x \in C \to (x \in \{x \in A \| B \neq \emptyset\} \leftrightarrow (x \in A \land B \neq \emptyset))$
18	15 17	mpbid	$⊢ x \in C \to (x \in A \land B \neq \emptyset)$
19	18	simprd	$⊢ x \in C \to B \neq \emptyset$
20	19	adantl	$⊢ (φ \land x \in C) \to B \neq \emptyset$
21	10	a1i	$⊢ φ \to C \subseteq A$
22		disjss1	$⊢ C \subseteq A \to (\underset{x \in A}{Disj} B \to \underset{x \in C}{Disj} B)$
23	21 4 22	sylc	$⊢ φ \to \underset{x \in C}{Disj} B$
24	1 7 14 20 23	disjf1	$⊢ φ \to (x \in C ⟼ B) : C \underset{1-1}{⟶} V$
25		f1f1orn	$⊢ (x \in C ⟼ B) : C \underset{1-1}{⟶} V \to (x \in C ⟼ B) : C \underset{1-1 onto}{⟶} ran (x \in C ⟼ B)$
26	24 25	syl	$⊢ φ \to (x \in C ⟼ B) : C \underset{1-1 onto}{⟶} ran (x \in C ⟼ B)$
27	2	a1i	$⊢ φ \to F = (x \in A ⟼ B)$
28	27	reseq1d	$⊢ φ \to {F ↾}_{C} = {(x \in A ⟼ B) ↾}_{C}$
29	21	resmptd	$⊢ φ \to {(x \in A ⟼ B) ↾}_{C} = (x \in C ⟼ B)$
30	28 29	eqtrd	$⊢ φ \to {F ↾}_{C} = (x \in C ⟼ B)$
31		eqidd	$⊢ φ \to C = C$
32		simpl	$⊢ (φ \land y \in D) \to φ$
33		id	$⊢ y \in D \to y \in D$
34	33 6	eleqtrdi	$⊢ y \in D \to y \in (ran F ∖ \{\emptyset\})$
35		eldifsni	$⊢ y \in (ran F ∖ \{\emptyset\}) \to y \neq \emptyset$
36	34 35	syl	$⊢ y \in D \to y \neq \emptyset$
37	36	adantl	$⊢ (φ \land y \in D) \to y \neq \emptyset$
38		eldifi	$⊢ y \in (ran F ∖ \{\emptyset\}) \to y \in ran F$
39	34 38	syl	$⊢ y \in D \to y \in ran F$
40	2	elrnmpt	$⊢ y \in ran F \to (y \in ran F \leftrightarrow \exists x \in A y = B)$
41	39 40	syl	$⊢ y \in D \to (y \in ran F \leftrightarrow \exists x \in A y = B)$
42	39 41	mpbid	$⊢ y \in D \to \exists x \in A y = B$
43	42	adantl	$⊢ (φ \land y \in D) \to \exists x \in A y = B$
44		nfv	$⊢ Ⅎ x y \neq \emptyset$
45	1 44	nfan	$⊢ Ⅎ x (φ \land y \neq \emptyset)$
46		nfcv	$⊢ \underline{Ⅎ} x y$
47		nfmpt1	$⊢ \underline{Ⅎ} x (x \in C ⟼ B)$
48	47	nfrn	$⊢ \underline{Ⅎ} x ran (x \in C ⟼ B)$
49	46 48	nfel	$⊢ Ⅎ x y \in ran (x \in C ⟼ B)$
50		simp3	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to y = B$
51		simp2	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to x \in A$
52		id	$⊢ y = B \to y = B$
53	52	eqcomd	$⊢ y = B \to B = y$
54	53	adantl	$⊢ (y \neq \emptyset \land y = B) \to B = y$
55		simpl	$⊢ (y \neq \emptyset \land y = B) \to y \neq \emptyset$
56	54 55	eqnetrd	$⊢ (y \neq \emptyset \land y = B) \to B \neq \emptyset$
57	56	3adant2	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to B \neq \emptyset$
58	51 57	jca	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to (x \in A \land B \neq \emptyset)$
59	58 16	sylibr	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to x \in \{x \in A \| B \neq \emptyset\}$
60	5	eqcomi	$⊢ \{x \in A \| B \neq \emptyset\} = C$
61	60	a1i	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to \{x \in A \| B \neq \emptyset\} = C$
62	59 61	eleqtrd	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to x \in C$
63		eqvisset	$⊢ y = B \to B \in V$
64	63	3ad2ant3	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to B \in V$
65	7	elrnmpt1	$⊢ (x \in C \land B \in V) \to B \in ran (x \in C ⟼ B)$
66	62 64 65	syl2anc	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to B \in ran (x \in C ⟼ B)$
67	50 66	eqeltrd	$⊢ (y \neq \emptyset \land x \in A \land y = B) \to y \in ran (x \in C ⟼ B)$
68	67	3adant1l	$⊢ ((φ \land y \neq \emptyset) \land x \in A \land y = B) \to y \in ran (x \in C ⟼ B)$
69	68	3exp	$⊢ (φ \land y \neq \emptyset) \to (x \in A \to (y = B \to y \in ran (x \in C ⟼ B)))$
70	45 49 69	rexlimd	$⊢ (φ \land y \neq \emptyset) \to (\exists x \in A y = B \to y \in ran (x \in C ⟼ B))$
71	70	imp	$⊢ ((φ \land y \neq \emptyset) \land \exists x \in A y = B) \to y \in ran (x \in C ⟼ B)$
72	32 37 43 71	syl21anc	$⊢ (φ \land y \in D) \to y \in ran (x \in C ⟼ B)$
73	72	ralrimiva	$⊢ φ \to \forall y \in D y \in ran (x \in C ⟼ B)$
74		dfss3	$⊢ D \subseteq ran (x \in C ⟼ B) \leftrightarrow \forall y \in D y \in ran (x \in C ⟼ B)$
75	73 74	sylibr	$⊢ φ \to D \subseteq ran (x \in C ⟼ B)$
76		simpl	$⊢ (φ \land y \in ran (x \in C ⟼ B)) \to φ$
77		vex	$⊢ y \in V$
78	7	elrnmpt	$⊢ y \in V \to (y \in ran (x \in C ⟼ B) \leftrightarrow \exists x \in C y = B)$
79	77 78	ax-mp	$⊢ y \in ran (x \in C ⟼ B) \leftrightarrow \exists x \in C y = B$
80	79	bilani	$⊢ (φ \land y \in ran (x \in C ⟼ B)) \to \exists x \in C y = B$
81		nfv	$⊢ Ⅎ x y \in D$
82		simpr	$⊢ (x \in C \land y = B) \to y = B$
83	12	adantr	$⊢ (x \in C \land y = B) \to x \in A$
84	82 63	syl	$⊢ (x \in C \land y = B) \to B \in V$
85	2	elrnmpt1	$⊢ (x \in A \land B \in V) \to B \in ran F$
86	83 84 85	syl2anc	$⊢ (x \in C \land y = B) \to B \in ran F$
87	82 86	eqeltrd	$⊢ (x \in C \land y = B) \to y \in ran F$
88	87	3adant1	$⊢ (φ \land x \in C \land y = B) \to y \in ran F$
89	19	adantr	$⊢ (x \in C \land y = B) \to B \neq \emptyset$
90	82 89	eqnetrd	$⊢ (x \in C \land y = B) \to y \neq \emptyset$
91		nelsn	$⊢ y \neq \emptyset \to \neg y \in \{\emptyset\}$
92	90 91	syl	$⊢ (x \in C \land y = B) \to \neg y \in \{\emptyset\}$
93	92	3adant1	$⊢ (φ \land x \in C \land y = B) \to \neg y \in \{\emptyset\}$
94	88 93	eldifd	$⊢ (φ \land x \in C \land y = B) \to y \in (ran F ∖ \{\emptyset\})$
95	94 6	eleqtrrdi	$⊢ (φ \land x \in C \land y = B) \to y \in D$
96	95	3exp	$⊢ φ \to (x \in C \to (y = B \to y \in D))$
97	1 81 96	rexlimd	$⊢ φ \to (\exists x \in C y = B \to y \in D)$
98	97	imp	$⊢ (φ \land \exists x \in C y = B) \to y \in D$
99	76 80 98	syl2anc	$⊢ (φ \land y \in ran (x \in C ⟼ B)) \to y \in D$
100	75 99	eqelssd	$⊢ φ \to D = ran (x \in C ⟼ B)$
101	30 31 100	f1oeq123d	$⊢ φ \to (({F ↾}_{C}) : C \underset{1-1 onto}{⟶} D \leftrightarrow (x \in C ⟼ B) : C \underset{1-1 onto}{⟶} ran (x \in C ⟼ B))$
102	26 101	mpbird	$⊢ φ \to ({F ↾}_{C}) : C \underset{1-1 onto}{⟶} D$

Metamath Proof Explorer

Theorem disjf1o

Proof