Step |
Hyp |
Ref |
Expression |
1 |
|
simplr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐶 <<s 𝐷 ) |
2 |
|
simpll |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐴 <<s 𝐵 ) |
3 |
|
simprr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑌 = ( 𝐶 |s 𝐷 ) ) |
4 |
|
simprl |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) ) |
5 |
|
slerec |
⊢ ( ( ( 𝐶 <<s 𝐷 ∧ 𝐴 <<s 𝐵 ) ∧ ( 𝑌 = ( 𝐶 |s 𝐷 ) ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ) ) ) |
6 |
1 2 3 4 5
|
syl22anc |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ) ) ) |
7 |
|
ancom |
⊢ ( ( ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ) ↔ ( ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ) ) |
8 |
6 7
|
bitrdi |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ) ) ) |
9 |
|
scutcut |
⊢ ( 𝐶 <<s 𝐷 → ( ( 𝐶 |s 𝐷 ) ∈ No ∧ 𝐶 <<s { ( 𝐶 |s 𝐷 ) } ∧ { ( 𝐶 |s 𝐷 ) } <<s 𝐷 ) ) |
10 |
9
|
simp1d |
⊢ ( 𝐶 <<s 𝐷 → ( 𝐶 |s 𝐷 ) ∈ No ) |
11 |
10
|
ad2antlr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝐶 |s 𝐷 ) ∈ No ) |
12 |
3 11
|
eqeltrd |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑌 ∈ No ) |
13 |
|
scutcut |
⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) |
14 |
13
|
simp1d |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ No ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝐴 |s 𝐵 ) ∈ No ) |
16 |
4 15
|
eqeltrd |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑋 ∈ No ) |
17 |
|
slenlt |
⊢ ( ( 𝑌 ∈ No ∧ 𝑋 ∈ No ) → ( 𝑌 ≤s 𝑋 ↔ ¬ 𝑋 <s 𝑌 ) ) |
18 |
12 16 17
|
syl2anc |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ¬ 𝑋 <s 𝑌 ) ) |
19 |
|
ssltss1 |
⊢ ( 𝐶 <<s 𝐷 → 𝐶 ⊆ No ) |
20 |
19
|
ad2antlr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐶 ⊆ No ) |
21 |
20
|
sselda |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ No ) |
22 |
16
|
adantr |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝑋 ∈ No ) |
23 |
|
sltnle |
⊢ ( ( 𝑐 ∈ No ∧ 𝑋 ∈ No ) → ( 𝑐 <s 𝑋 ↔ ¬ 𝑋 ≤s 𝑐 ) ) |
24 |
21 22 23
|
syl2anc |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝑐 <s 𝑋 ↔ ¬ 𝑋 ≤s 𝑐 ) ) |
25 |
24
|
ralbidva |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ↔ ∀ 𝑐 ∈ 𝐶 ¬ 𝑋 ≤s 𝑐 ) ) |
26 |
12
|
adantr |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑌 ∈ No ) |
27 |
|
ssltss2 |
⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No ) |
28 |
27
|
ad2antrr |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐵 ⊆ No ) |
29 |
28
|
sselda |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No ) |
30 |
|
sltnle |
⊢ ( ( 𝑌 ∈ No ∧ 𝑏 ∈ No ) → ( 𝑌 <s 𝑏 ↔ ¬ 𝑏 ≤s 𝑌 ) ) |
31 |
26 29 30
|
syl2anc |
⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑌 <s 𝑏 ↔ ¬ 𝑏 ≤s 𝑌 ) ) |
32 |
31
|
ralbidva |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 ≤s 𝑌 ) ) |
33 |
25 32
|
anbi12d |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ( ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ) ↔ ( ∀ 𝑐 ∈ 𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 ≤s 𝑌 ) ) ) |
34 |
|
ralnex |
⊢ ( ∀ 𝑐 ∈ 𝐶 ¬ 𝑋 ≤s 𝑐 ↔ ¬ ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ) |
35 |
|
ralnex |
⊢ ( ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 ≤s 𝑌 ↔ ¬ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) |
36 |
34 35
|
anbi12i |
⊢ ( ( ∀ 𝑐 ∈ 𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 ≤s 𝑌 ) ↔ ( ¬ ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∧ ¬ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) |
37 |
|
ioran |
⊢ ( ¬ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ↔ ( ¬ ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∧ ¬ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) |
38 |
36 37
|
bitr4i |
⊢ ( ( ∀ 𝑐 ∈ 𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏 ∈ 𝐵 ¬ 𝑏 ≤s 𝑌 ) ↔ ¬ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) |
39 |
33 38
|
bitrdi |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ( ∀ 𝑐 ∈ 𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏 ∈ 𝐵 𝑌 <s 𝑏 ) ↔ ¬ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) ) |
40 |
8 18 39
|
3bitr3d |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ¬ 𝑋 <s 𝑌 ↔ ¬ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) ) |
41 |
40
|
con4bid |
⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) ) |