Theorem elold

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

	Ref	Expression
Assertion	elold	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oldval	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
2	1	eleq2d	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ 𝑋 ∈ ∪ ( M “ 𝐴 ) ) )
3		eluni	⊢ ( 𝑋 ∈ ∪ ( M “ 𝐴 ) ↔ ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ 𝑦 ∈ ( M “ 𝐴 ) ) )
4		madef	⊢ M : On ⟶ 𝒫 No
5		ffn	⊢ ( M : On ⟶ 𝒫 No → M Fn On )
6	4 5	ax-mp	⊢ M Fn On
7		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
8		fvelimab	⊢ ( ( M Fn On ∧ 𝐴 ⊆ On ) → ( 𝑦 ∈ ( M “ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) )
9	6 7 8	sylancr	⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ ( M “ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) )
10	9	anbi2d	⊢ ( 𝐴 ∈ On → ( ( 𝑋 ∈ 𝑦 ∧ 𝑦 ∈ ( M “ 𝐴 ) ) ↔ ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) ) )
11	10	exbidv	⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ 𝑦 ∈ ( M “ 𝐴 ) ) ↔ ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) ) )
12		fvex	⊢ ( M ‘ 𝑏 ) ∈ V
13	12	clel3	⊢ ( 𝑋 ∈ ( M ‘ 𝑏 ) ↔ ∃ 𝑦 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) )
14	13	rexbii	⊢ ( ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) )
15		rexcom4	⊢ ( ∃ 𝑏 ∈ 𝐴 ∃ 𝑦 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) ↔ ∃ 𝑦 ∃ 𝑏 ∈ 𝐴 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) )
16		eqcom	⊢ ( 𝑦 = ( M ‘ 𝑏 ) ↔ ( M ‘ 𝑏 ) = 𝑦 )
17	16	anbi2ci	⊢ ( ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) ↔ ( 𝑋 ∈ 𝑦 ∧ ( M ‘ 𝑏 ) = 𝑦 ) )
18	17	rexbii	⊢ ( ∃ 𝑏 ∈ 𝐴 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) ↔ ∃ 𝑏 ∈ 𝐴 ( 𝑋 ∈ 𝑦 ∧ ( M ‘ 𝑏 ) = 𝑦 ) )
19		r19.42v	⊢ ( ∃ 𝑏 ∈ 𝐴 ( 𝑋 ∈ 𝑦 ∧ ( M ‘ 𝑏 ) = 𝑦 ) ↔ ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) )
20	18 19	bitri	⊢ ( ∃ 𝑏 ∈ 𝐴 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) ↔ ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) )
21	20	exbii	⊢ ( ∃ 𝑦 ∃ 𝑏 ∈ 𝐴 ( 𝑦 = ( M ‘ 𝑏 ) ∧ 𝑋 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) )
22	14 15 21	3bitrri	⊢ ( ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ ∃ 𝑏 ∈ 𝐴 ( M ‘ 𝑏 ) = 𝑦 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) )
23	11 22	bitrdi	⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ( 𝑋 ∈ 𝑦 ∧ 𝑦 ∈ ( M “ 𝐴 ) ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )
24	3 23	syl5bb	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ∪ ( M “ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )
25	2 24	bitrd	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )