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 ‘ 𝐴 ) )