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 ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → ( 𝐿 |s 𝑅 ) ∈ ( M ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simplr ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝐿 <<s 𝑅 )
2 ssltex1 ( 𝐿 <<s 𝑅𝐿 ∈ V )
3 1 2 syl ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝐿 ∈ V )
4 simprl ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝐿 ⊆ ( O ‘ 𝐴 ) )
5 3 4 elpwd ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝐿 ∈ 𝒫 ( O ‘ 𝐴 ) )
6 ssltex2 ( 𝐿 <<s 𝑅𝑅 ∈ V )
7 1 6 syl ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝑅 ∈ V )
8 simprr ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝑅 ⊆ ( O ‘ 𝐴 ) )
9 7 8 elpwd ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → 𝑅 ∈ 𝒫 ( O ‘ 𝐴 ) )
10 eqidd ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → ( 𝐿 |s 𝑅 ) = ( 𝐿 |s 𝑅 ) )
11 breq1 ( 𝑙 = 𝐿 → ( 𝑙 <<s 𝑟𝐿 <<s 𝑟 ) )
12 oveq1 ( 𝑙 = 𝐿 → ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑟 ) )
13 12 eqeq1d ( 𝑙 = 𝐿 → ( ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ↔ ( 𝐿 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) )
14 11 13 anbi12d ( 𝑙 = 𝐿 → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) ↔ ( 𝐿 <<s 𝑟 ∧ ( 𝐿 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) ) )
15 breq2 ( 𝑟 = 𝑅 → ( 𝐿 <<s 𝑟𝐿 <<s 𝑅 ) )
16 oveq2 ( 𝑟 = 𝑅 → ( 𝐿 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) )
17 16 eqeq1d ( 𝑟 = 𝑅 → ( ( 𝐿 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ↔ ( 𝐿 |s 𝑅 ) = ( 𝐿 |s 𝑅 ) ) )
18 15 17 anbi12d ( 𝑟 = 𝑅 → ( ( 𝐿 <<s 𝑟 ∧ ( 𝐿 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) ↔ ( 𝐿 <<s 𝑅 ∧ ( 𝐿 |s 𝑅 ) = ( 𝐿 |s 𝑅 ) ) ) )
19 14 18 rspc2ev ( ( 𝐿 ∈ 𝒫 ( O ‘ 𝐴 ) ∧ 𝑅 ∈ 𝒫 ( O ‘ 𝐴 ) ∧ ( 𝐿 <<s 𝑅 ∧ ( 𝐿 |s 𝑅 ) = ( 𝐿 |s 𝑅 ) ) ) → ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) )
20 5 9 1 10 19 syl112anc ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) )
21 elmade2 ( 𝐴 ∈ On → ( ( 𝐿 |s 𝑅 ) ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) ) )
22 21 ad2antrr ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → ( ( 𝐿 |s 𝑅 ) ∈ ( M ‘ 𝐴 ) ↔ ∃ 𝑙 ∈ 𝒫 ( O ‘ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ( O ‘ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = ( 𝐿 |s 𝑅 ) ) ) )
23 20 22 mpbird ( ( ( 𝐴 ∈ On ∧ 𝐿 <<s 𝑅 ) ∧ ( 𝐿 ⊆ ( O ‘ 𝐴 ) ∧ 𝑅 ⊆ ( O ‘ 𝐴 ) ) ) → ( 𝐿 |s 𝑅 ) ∈ ( M ‘ 𝐴 ) )