f1ossf1o

Description: Restricting a bijection, which is a mapping from a restricted class abstraction, to a subset is a bijection. (Contributed by AV, 7-Aug-2022)

	Ref	Expression
Hypotheses	f1ossf1o.x	$⊢ X = \{w \in A \| (ψ \land χ)\}$
	f1ossf1o.y	$⊢ Y = \{w \in A \| ψ\}$
	f1ossf1o.f	$⊢ F = (x \in X ⟼ B)$
	f1ossf1o.g	$⊢ G = (x \in Y ⟼ B)$
	f1ossf1o.b	$⊢ φ \to G : Y \underset{1-1 onto}{⟶} C$
	f1ossf1o.s	$⊢ (φ \land x \in Y \land y = B) \to (τ \leftrightarrow [x/ w] χ)$
Assertion	f1ossf1o	$⊢ φ \to F : X \underset{1-1 onto}{⟶} \{y \in C \| τ\}$

Proof

Step	Hyp	Ref	Expression
1		f1ossf1o.x	$⊢ X = \{w \in A \| (ψ \land χ)\}$
2		f1ossf1o.y	$⊢ Y = \{w \in A \| ψ\}$
3		f1ossf1o.f	$⊢ F = (x \in X ⟼ B)$
4		f1ossf1o.g	$⊢ G = (x \in Y ⟼ B)$
5		f1ossf1o.b	$⊢ φ \to G : Y \underset{1-1 onto}{⟶} C$
6		f1ossf1o.s	$⊢ (φ \land x \in Y \land y = B) \to (τ \leftrightarrow [x/ w] χ)$
7	4 5 6	f1oresrab	$⊢ φ \to ({G ↾}_{\{x \in Y \| [x/ w] χ\}}) : \{x \in Y \| [x/ w] χ\} \underset{1-1 onto}{⟶} \{y \in C \| τ\}$
8		simpl	$⊢ (ψ \land χ) \to ψ$
9	8	a1i	$⊢ w \in A \to ((ψ \land χ) \to ψ)$
10	9	ss2rabi	$⊢ \{w \in A \| (ψ \land χ)\} \subseteq \{w \in A \| ψ\}$
11	10 1 2	3sstr4i	$⊢ X \subseteq Y$
12	11	a1i	$⊢ φ \to X \subseteq Y$
13	12	resmptd	$⊢ φ \to {(x \in Y ⟼ B) ↾}_{X} = (x \in X ⟼ B)$
14	4	a1i	$⊢ φ \to G = (x \in Y ⟼ B)$
15	2	rabeqi	$⊢ \{x \in Y \| [x/ w] χ\} = \{x \in \{w \in A \| ψ\} \| [x/ w] χ\}$
16		nfcv	$⊢ \underline{Ⅎ} w x$
17		nfcv	$⊢ \underline{Ⅎ} w A$
18		nfs1v	$⊢ Ⅎ w [x/ w] ψ$
19		sbequ12	$⊢ w = x \to (ψ \leftrightarrow [x/ w] ψ)$
20	16 17 18 19	elrabf	$⊢ x \in \{w \in A \| ψ\} \leftrightarrow (x \in A \land [x/ w] ψ)$
21	20	anbi1i	$⊢ (x \in \{w \in A \| ψ\} \land [x/ w] χ) \leftrightarrow ((x \in A \land [x/ w] ψ) \land [x/ w] χ)$
22		anass	$⊢ ((x \in A \land [x/ w] ψ) \land [x/ w] χ) \leftrightarrow (x \in A \land ([x/ w] ψ \land [x/ w] χ))$
23	21 22	bitri	$⊢ (x \in \{w \in A \| ψ\} \land [x/ w] χ) \leftrightarrow (x \in A \land ([x/ w] ψ \land [x/ w] χ))$
24	23	rabbia2	$⊢ \{x \in \{w \in A \| ψ\} \| [x/ w] χ\} = \{x \in A \| ([x/ w] ψ \land [x/ w] χ)\}$
25		nfcv	$⊢ \underline{Ⅎ} x A$
26		nfv	$⊢ Ⅎ x (ψ \land χ)$
27		nfs1v	$⊢ Ⅎ w [x/ w] χ$
28	18 27	nfan	$⊢ Ⅎ w ([x/ w] ψ \land [x/ w] χ)$
29		sbequ12	$⊢ w = x \to (χ \leftrightarrow [x/ w] χ)$
30	19 29	anbi12d	$⊢ w = x \to ((ψ \land χ) \leftrightarrow ([x/ w] ψ \land [x/ w] χ))$
31	17 25 26 28 30	cbvrabw	$⊢ \{w \in A \| (ψ \land χ)\} = \{x \in A \| ([x/ w] ψ \land [x/ w] χ)\}$
32	1 31	eqtr2i	$⊢ \{x \in A \| ([x/ w] ψ \land [x/ w] χ)\} = X$
33	15 24 32	3eqtri	$⊢ \{x \in Y \| [x/ w] χ\} = X$
34	33	a1i	$⊢ φ \to \{x \in Y \| [x/ w] χ\} = X$
35	14 34	reseq12d	$⊢ φ \to {G ↾}_{\{x \in Y \| [x/ w] χ\}} = {(x \in Y ⟼ B) ↾}_{X}$
36	3	a1i	$⊢ φ \to F = (x \in X ⟼ B)$
37	13 35 36	3eqtr4rd	$⊢ φ \to F = {G ↾}_{\{x \in Y \| [x/ w] χ\}}$
38	15 24	eqtr2i	$⊢ \{x \in A \| ([x/ w] ψ \land [x/ w] χ)\} = \{x \in Y \| [x/ w] χ\}$
39	1 31 38	3eqtri	$⊢ X = \{x \in Y \| [x/ w] χ\}$
40	39	a1i	$⊢ φ \to X = \{x \in Y \| [x/ w] χ\}$
41		eqidd	$⊢ φ \to \{y \in C \| τ\} = \{y \in C \| τ\}$
42	37 40 41	f1oeq123d	$⊢ φ \to (F : X \underset{1-1 onto}{⟶} \{y \in C \| τ\} \leftrightarrow ({G ↾}_{\{x \in Y \| [x/ w] χ\}}) : \{x \in Y \| [x/ w] χ\} \underset{1-1 onto}{⟶} \{y \in C \| τ\})$
43	7 42	mpbird	$⊢ φ \to F : X \underset{1-1 onto}{⟶} \{y \in C \| τ\}$

Metamath Proof Explorer

Theorem f1ossf1o

Proof