Metamath Proof Explorer

Theorem madecut

Description: Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion madecut ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L | s R ∈ M ⁡ A

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L ≪ s R
2 sltsex1 ⊢ L ≪ s R → L ∈ V
3 1 2 syl ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L ∈ V
4 simprl ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L ⊆ Old ⁡ A
5 3 4 elpwd ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L ∈ 𝒫 Old ⁡ A
6 sltsex2 ⊢ L ≪ s R → R ∈ V
7 1 6 syl ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → R ∈ V
8 simprr ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → R ⊆ Old ⁡ A
9 7 8 elpwd ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → R ∈ 𝒫 Old ⁡ A
10 eqidd ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L | s R = L | s R
11 breq1 ⊢ l = L → l ≪ s r ↔ L ≪ s r
12 oveq1 ⊢ l = L → l | s r = L | s r
13 12 eqeq1d ⊢ l = L → l | s r = L | s R ↔ L | s r = L | s R
14 11 13 anbi12d ⊢ l = L → l ≪ s r ∧ l | s r = L | s R ↔ L ≪ s r ∧ L | s r = L | s R
15 breq2 ⊢ r = R → L ≪ s r ↔ L ≪ s R
16 oveq2 ⊢ r = R → L | s r = L | s R
17 16 eqeq1d ⊢ r = R → L | s r = L | s R ↔ L | s R = L | s R
18 15 17 anbi12d ⊢ r = R → L ≪ s r ∧ L | s r = L | s R ↔ L ≪ s R ∧ L | s R = L | s R
19 14 18 rspc2ev ⊢ L ∈ 𝒫 Old ⁡ A ∧ R ∈ 𝒫 Old ⁡ A ∧ L ≪ s R ∧ L | s R = L | s R → ∃ l ∈ 𝒫 Old ⁡ A ∃ r ∈ 𝒫 Old ⁡ A l ≪ s r ∧ l | s r = L | s R
20 5 9 1 10 19 syl112anc ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → ∃ l ∈ 𝒫 Old ⁡ A ∃ r ∈ 𝒫 Old ⁡ A l ≪ s r ∧ l | s r = L | s R
21 elmade2 ⊢ A ∈ On → L | s R ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 Old ⁡ A ∃ r ∈ 𝒫 Old ⁡ A l ≪ s r ∧ l | s r = L | s R
22 21 ad2antrr ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L | s R ∈ M ⁡ A ↔ ∃ l ∈ 𝒫 Old ⁡ A ∃ r ∈ 𝒫 Old ⁡ A l ≪ s r ∧ l | s r = L | s R
23 20 22 mpbird ⊢ A ∈ On ∧ L ≪ s R ∧ L ⊆ Old ⁡ A ∧ R ⊆ Old ⁡ A → L | s R ∈ M ⁡ A