riotass2

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)

		Ref	Expression
	Assertion	riotass2	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (ι x \in A \| φ) = (ι x \in B \| ψ)$

Proof

Step	Hyp	Ref	Expression
1		reuss2	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \exists! x \in A φ$
2		simplr	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \forall x \in A (φ \to ψ)$
3		riotasbc	$⊢ \exists! x \in A φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ$
4		riotacl	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) \in A$
5		rspsbc	$⊢ (ι x \in A \| φ) \in A \to (\forall x \in A (φ \to ψ) \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} (φ \to ψ))$
6		sbcimg	$⊢ (ι x \in A \| φ) \in A \to (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} (φ \to ψ) \leftrightarrow (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ))$
7	5 6	sylibd	$⊢ (ι x \in A \| φ) \in A \to (\forall x \in A (φ \to ψ) \to (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ))$
8	4 7	syl	$⊢ \exists! x \in A φ \to (\forall x \in A (φ \to ψ) \to (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} φ \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ))$
9	3 8	mpid	$⊢ \exists! x \in A φ \to (\forall x \in A (φ \to ψ) \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ)$
10	1 2 9	sylc	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ$
11	1 4	syl	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (ι x \in A \| φ) \in A$
12		ssel	$⊢ A \subseteq B \to ((ι x \in A \| φ) \in A \to (ι x \in A \| φ) \in B)$
13	12	ad2antrr	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to ((ι x \in A \| φ) \in A \to (ι x \in A \| φ) \in B)$
14	11 13	mpd	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (ι x \in A \| φ) \in B$
15		simprr	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to \exists! x \in B ψ$
16		nfriota1	$⊢ \underline{Ⅎ} x (ι x \in A \| φ)$
17	16	nfsbc1	$⊢ Ⅎ x \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ$
18		sbceq1a	$⊢ x = (ι x \in A \| φ) \to (ψ \leftrightarrow \underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ)$
19	16 17 18	riota2f	$⊢ ((ι x \in A \| φ) \in B \land \exists! x \in B ψ) \to (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ \leftrightarrow (ι x \in B \| ψ) = (ι x \in A \| φ))$
20	14 15 19	syl2anc	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (\underset{˙}{[} (ι x \in A \| φ) / x \underset{˙}{]} ψ \leftrightarrow (ι x \in B \| ψ) = (ι x \in A \| φ))$
21	10 20	mpbid	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (ι x \in B \| ψ) = (ι x \in A \| φ)$
22	21	eqcomd	$⊢ ((A \subseteq B \land \forall x \in A (φ \to ψ)) \land (\exists x \in A φ \land \exists! x \in B ψ)) \to (ι x \in A \| φ) = (ι x \in B \| ψ)$

Metamath Proof Explorer

Theorem riotass2

Proof