elold

Description: Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024)

		Ref	Expression
	Assertion	elold	$⊢ A \in On \to (X \in Old (A) \leftrightarrow \exists b \in A X \in M (b))$

Proof

Step	Hyp	Ref	Expression
1		oldval	$⊢ A \in On \to Old (A) = ⋃ M [A]$
2	1	eleq2d	$⊢ A \in On \to (X \in Old (A) \leftrightarrow X \in ⋃ M [A])$
3		eluni	$⊢ X \in ⋃ M [A] \leftrightarrow \exists y (X \in y \land y \in M [A])$
4		madef	$⊢ M : On ⟶ 𝒫 No$
5		ffn	$⊢ M : On ⟶ 𝒫 No \to M Fn On$
6	4 5	ax-mp	$⊢ M Fn On$
7		onss	$⊢ A \in On \to A \subseteq On$
8		fvelimab	$⊢ (M Fn On \land A \subseteq On) \to (y \in M [A] \leftrightarrow \exists b \in A M (b) = y)$
9	6 7 8	sylancr	$⊢ A \in On \to (y \in M [A] \leftrightarrow \exists b \in A M (b) = y)$
10	9	anbi2d	$⊢ A \in On \to ((X \in y \land y \in M [A]) \leftrightarrow (X \in y \land \exists b \in A M (b) = y))$
11	10	exbidv	$⊢ A \in On \to (\exists y (X \in y \land y \in M [A]) \leftrightarrow \exists y (X \in y \land \exists b \in A M (b) = y))$
12		fvex	$⊢ M (b) \in V$
13	12	clel3	$⊢ X \in M (b) \leftrightarrow \exists y (y = M (b) \land X \in y)$
14	13	rexbii	$⊢ \exists b \in A X \in M (b) \leftrightarrow \exists b \in A \exists y (y = M (b) \land X \in y)$
15		rexcom4	$⊢ \exists b \in A \exists y (y = M (b) \land X \in y) \leftrightarrow \exists y \exists b \in A (y = M (b) \land X \in y)$
16		eqcom	$⊢ y = M (b) \leftrightarrow M (b) = y$
17	16	anbi2ci	$⊢ (y = M (b) \land X \in y) \leftrightarrow (X \in y \land M (b) = y)$
18	17	rexbii	$⊢ \exists b \in A (y = M (b) \land X \in y) \leftrightarrow \exists b \in A (X \in y \land M (b) = y)$
19		r19.42v	$⊢ \exists b \in A (X \in y \land M (b) = y) \leftrightarrow (X \in y \land \exists b \in A M (b) = y)$
20	18 19	bitri	$⊢ \exists b \in A (y = M (b) \land X \in y) \leftrightarrow (X \in y \land \exists b \in A M (b) = y)$
21	20	exbii	$⊢ \exists y \exists b \in A (y = M (b) \land X \in y) \leftrightarrow \exists y (X \in y \land \exists b \in A M (b) = y)$
22	14 15 21	3bitrri	$⊢ \exists y (X \in y \land \exists b \in A M (b) = y) \leftrightarrow \exists b \in A X \in M (b)$
23	11 22	bitrdi	$⊢ A \in On \to (\exists y (X \in y \land y \in M [A]) \leftrightarrow \exists b \in A X \in M (b))$
24	3 23	bitrid	$⊢ A \in On \to (X \in ⋃ M [A] \leftrightarrow \exists b \in A X \in M (b))$
25	2 24	bitrd	$⊢ A \in On \to (X \in Old (A) \leftrightarrow \exists b \in A X \in M (b))$

Metamath Proof Explorer

Theorem elold

Proof