Metamath Proof Explorer

Theorem elold

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

Ref Expression
Assertion elold ⊢ A ∈ On → X ∈ Old ⁡ A ↔ ∃ b ∈ A X ∈ M ⁡ b

Proof

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