Metamath Proof Explorer

Theorem elmade

Description: Membership in the made function. (Contributed by Scott Fenton, 6-Aug-2024)

Ref Expression
Assertion elmade ⊢ A ∈ On → X ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X

Proof

Step Hyp Ref Expression
1 madef ⊢ M : On ⟶ 𝒫 No
2 1 ffvelrni ⊢ A ∈ On → M ⁡ A ∈ 𝒫 No
3 2 elpwid ⊢ A ∈ On → M ⁡ A ⊆ No
4 3 sseld ⊢ A ∈ On → X ∈ M ⁡ A → X ∈ No
5 scutcl ⊢ l ≪ s r → l | s r ∈ No
6 eleq1 ⊢ l | s r = X → l | s r ∈ No ↔ X ∈ No
7 6 biimpd ⊢ l | s r = X → l | s r ∈ No → X ∈ No
8 5 7 mpan9 ⊢ l ≪ s r ∧ l | s r = X → X ∈ No
9 8 rexlimivw ⊢ ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X → X ∈ No
10 9 rexlimivw ⊢ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X → X ∈ No
11 10 a1i ⊢ A ∈ On → ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X → X ∈ No
12 madeval2 ⊢ A ∈ On → M ⁡ A = x ∈ No | ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = x
13 12 eleq2d ⊢ A ∈ On → X ∈ M ⁡ A ↔ X ∈ x ∈ No | ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = x
14 eqeq2 ⊢ x = X → l | s r = x ↔ l | s r = X
15 14 anbi2d ⊢ x = X → l ≪ s r ∧ l | s r = x ↔ l ≪ s r ∧ l | s r = X
16 15 2rexbidv ⊢ x = X → ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = x ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X
17 16 elrab3 ⊢ X ∈ No → X ∈ x ∈ No | ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = x ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X
18 13 17 sylan9bb ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X
19 18 ex ⊢ A ∈ On → X ∈ No → X ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X
20 4 11 19 pm5.21ndd ⊢ A ∈ On → X ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 ⋃ M A ∃ r ∈ 𝒫 ⋃ M A l ≪ s r ∧ l | s r = X