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