rightf

Description: The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024)

		Ref	Expression
	Assertion	rightf	Could not format assertion : No typesetting found for \|- _Right : No --> ~P No with typecode \|-

Step	Hyp	Ref	Expression
1		df-right	Could not format _Right = ( x e. No \|-> { y e. ( _Old ` ( bday ` x ) ) \| x ~~{ y e. ( _Old ` ( bday ` x ) ) \| x~~
2		bdayelon	$⊢ bday (x) \in On$
3		oldf	$⊢ Old : On ⟶ 𝒫 No$
4	3	ffvelcdmi	$⊢ bday (x) \in On \to Old (bday (x)) \in 𝒫 No$
5	2 4	mp1i	$⊢ x \in No \to Old (bday (x)) \in 𝒫 No$
6	5	elpwid	$⊢ x \in No \to Old (bday (x)) \subseteq No$
7	6	sselda	$⊢ (x \in No \land y \in Old (bday (x))) \to y \in No$
8	7	a1d	$⊢ (x \in No \land y \in Old (bday (x))) \to (x <_{s} y \to y \in No)$
9	8	ralrimiva	$⊢ x \in No \to \forall y \in Old (bday (x)) (x <_{s} y \to y \in No)$
10		fvex	$⊢ Old (bday (x)) \in V$
11	10	rabex	$⊢ \{y \in Old (bday (x)) \| x <_{s} y\} \in V$
12	11	elpw	$⊢ \{y \in Old (bday (x)) \| x <_{s} y\} \in 𝒫 No \leftrightarrow \{y \in Old (bday (x)) \| x <_{s} y\} \subseteq No$
13		rabss	$⊢ \{y \in Old (bday (x)) \| x <_{s} y\} \subseteq No \leftrightarrow \forall y \in Old (bday (x)) (x <_{s} y \to y \in No)$
14	12 13	bitri	$⊢ \{y \in Old (bday (x)) \| x <_{s} y\} \in 𝒫 No \leftrightarrow \forall y \in Old (bday (x)) (x <_{s} y \to y \in No)$
15	9 14	sylibr	$⊢ x \in No \to \{y \in Old (bday (x)) \| x <_{s} y\} \in 𝒫 No$
16	1 15	fmpti	Could not format _Right : No --> ~P No : No typesetting found for \|- _Right : No --> ~P No with typecode \|-

Metamath Proof Explorer